Sciweavers

Share
ICALP
2000
Springer

Decidable First-Order Transition Logics for PA-Processes

10 years 5 months ago
Decidable First-Order Transition Logics for PA-Processes
We show the decidability of model checking PA-processes against several first-order logics based upon the reachability predicate. The main tool for this result is the recognizability by tree automata of the reachability relation. The tree automata approach and the transition logics we use allow a smooth and general treatment of parameterized model checking for PA. This approach is extended to handle a quite general notion of costs of PA-steps. In particular, when costs are Parikh images of traces, we show decidability of a transition logic extended by some form of first-order reasoning over costs. Key words: Regular model checking, Verification of recursive parallel systems, Transition logics, Regular tree languages
Denis Lugiez, Ph. Schnoebelen
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Where ICALP
Authors Denis Lugiez, Ph. Schnoebelen
Comments (0)
books