We show decidability of several first-order logics based upon the reachability predicate in PA. The main tool we use is the recognizability by tree automata of the reachability relation between PA-processes. This approach and the transition logics we use allow a smooth and general treatment of parameterized model checking for PA. Then the logic is extended to handle a 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.
CITATION STYLE
Lugiez, D., & Schnoebelen, P. (2000). Decidable first-order transition logics for PA-processes. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1853, pp. 342–353). Springer Verlag. https://doi.org/10.1007/3-540-45022-x_30
Mendeley helps you to discover research relevant for your work.