NDLI: Model checking synchronized products of infinite transition systems

Content Provider	IEEE Xplore Digital Library
Author	Wohrle, S. Thomas, W.
Copyright Year	2004
Description	Author affiliation: Lehrstuhl fur Informatik 7, RWTH, Aachen, Germany (Wohrle, S.; Thomas, W.)
Abstract	Formal verification using the model-checking paradigm has to deal with two aspects. The systems models are structured, often as products of components, and the specification logic has to be expressive enough to allow the formalization of reachability properties. The present paper is a study on what can be achieved for infinite transition systems under these premises. As models, we consider products of infinite transition systems with different synchronization constraints. We introduce finitely synchronized transition systems, i.e. product systems which contain only finitely many synchronized transitions, and show that the decidability of FO(R), first-order logic extended by reachability predicates, of the product system can be reduced to the decidability of FO(R) of the components in a Feferman-Vaught like style. This result is optimal in the following sense. (1) If we allow semifinite synchronization, i.e. just in one component infinitely many transitions are synchronized, the FO(R)-theory of the product system is in general undecidable. (2) We cannot extend the expressive power of the logic under consideration. Already a weak extension of first-order logic with transitive closure, where we restrict the transitive closure operators to arity one and nesting depth two, is undecidable for an asynchronous (and hence finitely synchronized) product, namely for the infinite grid.
Sponsorship	IEEE Comput. Soc. Tech. Committee on Math. Found. on Comput
Starting Page	2
Ending Page	11
File Size	561974
Page Count	10
File Format	PDF
ISBN	0769521924
ISSN	10436871
DOI	10.1109/LICS.2004.1319595
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2004-07-17
Publisher Place	Finland
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Logic Filters Computational modeling Computer science
Content Type	Text
Resource Type	Article
Subject	Mathematics Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Model Checking Synchronized Products of Infinite Transition Systems

Model checking synchronized products of infinite transition systems.

Model checking synchronized products of infinite transition systems (2004)

A classification of symbolic transition systems

Multi-valued Modal Fixed Point Logics for Model Checking

Bounded model checking of infinite state systems: exploiting the automata hierarchy

Bounded model checking of infinite state systems

Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata

A Computational Method for Temporal Logic Reasoning and Model Checking

Model checking synchronized products of infinite transition systems

Similar Documents

Model Checking Synchronized Products of Infinite Transition Systems

Model checking synchronized products of infinite transition systems.

Model checking synchronized products of infinite transition systems (2004)

A classification of symbolic transition systems

Multi-valued Modal Fixed Point Logics for Model Checking

Bounded model checking of infinite state systems: exploiting the automata hierarchy

Bounded model checking of infinite state systems

Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata

A Computational Method for Temporal Logic Reasoning and Model Checking

Model checking synchronized products of infinite transition systems