Model Checking Synchronized Products of Infinite Transition Systems

Details Model Checking Synchronized Products of Infinite Transition Systems Model Checking Synchronized Products of Infinite Transition Systems

2007-10-30

arxiv.org/abs/0710.5659v2

LMCS 3 (4:5) 2007

Computer Science

Logic in Computer Science

18 pages

Scientific paper

10.2168/LMCS-3(4:5)2007

Formal verification using the model checking paradigm has to deal with two aspects: The system 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 (parameterized) 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. 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.

Affiliated with

Also associated with

No associations

Rating

Model Checking Synchronized Products of Infinite Transition Systems does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Model Checking Synchronized Products of Infinite Transition Systems, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Model Checking Synchronized Products of Infinite Transition Systems will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-365589