Volume: 20, Issue: 5(2009)
pp. 851-868 DOI: 10.1142/S0129054109006929
|
|
Abstract |
Full Text (PDF, 316KB)
|
References
|
 |
| Title: |
COMPOSITIONALITY AND REACHABILITY WITH CONDITIONS ON PATH LENGTHS |
| Author(s): |
INGO FELSCHER
http://www.automata.rwth-aachen.de/~felscher/
Lehrstuhl Informatik 7, RWTH Aachen University, Ahornstrasse 55, 52074 Aachen, GermanyWOLFGANG THOMAS
http://www.automata.rwth-aachen.de/~thomas/
Lehrstuhl Informatik 7, RWTH Aachen University, Ahornstrasse 55, 52074 Aachen, Germany
|
| History: |
Received 5 December 2008
Accepted 15 May 2009
|
| Abstract: |
In model-checking the systems under investigation often arise in the form of products. The compositional method, developed by Feferman and Vaught in 1959, fits to this situation and can be used to deduce the truth of a formula in the product from information in the factors. Building on earlier work of Wöhrle and Thomas (2004), we study first-order logic with reachability predicates over finitely synchronized products (i.e. synchronized products with a finite number of synchronization transitions). We extend the reachability predicates by conditions on the length of the corresponding paths, formulated in Presburger arithmetic. For finitely synchronized products with these enhanced reachability predicates we prove a composition theorem and then show that severe limitations exist for generalisations of this result. |
| Keywords: |
Feferman-Vaught Theorem; composition theorem; finitely synchronized products; Presburger arithmetic
|
|
|
