Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, K. Etessami, S. La Torre, and D. Peled. Parametric temporal logic for “model measuring”. In Proc. 26th Int. Coll. Automata, Languages, and Programming, vol. 1644 of L.N.C.S., pages 159–168. Springer, 1999.
R. Alur and T. A. Henzinger. A really temporal logic. J. of the ACM, 41(1):181–203, 1994.
A. Bouajjani, R. Echahed, and P. Habermehl. On the verification problem of nonregular properties for nonregular processes. In Proc. 10th IEEE Symp. Logic Comp. Science, pages 123–133, 1995.
A. Bouajjani, R. Echahed, and P. Habermehl. Verifying infinite state processes with sequential and parallel composition. In Proc. 22nd ACM Symp. Princ. of Programming Languages, pages 95–106, 1995.
J. C. M. Baeten and W. P. Weijland. Process Algebra, vol. 18 of Cambridge Tracts in Theoretical Computer Science. Cambridge Univ. Press, 1990.
H. Comon, M. Dauchet, R. Gilleron, D. Lugiez, S. Tison, and M. Tommasi. Tree Automata Techniques and Applications, 1997–99. Available at http://www.grappa.univ-lille3.fr/tata.
H. Comon and Y. Jurski. Timed automata and the theory of real numbers. In Proc. 10th Int. Conf. Concurrency Theory, vol. 1664 of L.N.C.S., pages 242–257. Springer, 1999.
M. Dauchet and S. Tison. The theory of ground rewrite systems is decidable. In Proc. 5th IEEE Symp. Logic in Computer Science, pages 242–248, 1990.
J. Esparza and J. Knoop. An automata-theoretic approach to interprocedural dataflow analysis. In Proc. 2nd Int. Conf. Found. of Soft. Sci. and Comp. Struct., vol. 1578 of L.N.C.S., pages 14–30. Springer, 1999.
J. Esparza and A. Podelski. Efficient algorithms for pre* and post* on interprocedural parallel flow graphs. In Proc. 27th ACM Symp. Principles of Programming Languages, 2000.
J. Esparza. Petri nets, commutative context-free grammars, and basic parallel processes. Fundamenta Informaticae, 31(1):13–25, 1997.
E. A. Emerson and R. J. Treer. Parametric quantitative temporal reasoning. In Proc. 14th IEEE Symp. Logic in Comp. Sci., pp 336–343, 1999.
Y. Hirshfeld and M. Jerrum. Bisimulation equivalence is decidable for normed process algebra. In Proc. 26th Int. Coll. Automata, Languages, and Programming, vol. 1644 of L.N.C.S., pages 412–421. Springer, 1999.
P. Jançar, A. Kučera, and R. Mayr. Deciding bisimulation-like equivalences with finite-state 201 449 243 461 processes. In Proc. 25th Int. Coll. Automata, Languages, and Programming, vol. 1443 of L.N.C.S., pages 200–211. Springer, 1998.
A. Kučera. Regularity is decidable for normed PA processes in polynomial time. In Proc. 16th Conf. Found. of Software Technology and Theor. Comp. Sci., vol. 1180 of L.N.C.S., pages 111–122. Springer, 1996.
A. Kučera. How to parallelize sequential processes. In Proc. 8th Int. Conf. Concurrency Theory, vol. 1243 of L.N.C. S., pages 302–316. Springer, 1997.
D. Lugiez and Ph. Schnoebelen. The regular viewpoint on PA-processes. September1999. To appear in Theor. Comp. Sci.
R. Mayr. Tableaux methods for PA-processes. In Proc. TABLEAUX’97, vol. 1227 of L.N.A.I., pages 276–290. Springer, 1997.
R. Mayr. Decidability of model checking with the temporal logic EF. May 1999. To appear in Theor. Comp. Sci.
R. Mayr. Process rewrite systems. Information and Computation, 156(1/2):264–286, 2000.
F. Moller. Infinite results. In Proc. 7th Int. Conf. Concurrency Theory, vol. 1119 of L.N.C.S., pages 195–216. Springer, 1996.
R. J. Parikh. On context-free languages. J.A.C.M, 13(4):570–581, 1966.
G. D. Plotkin. A structural approach to operational semantics. Lect. Notes, Aarhus University, Aarhus, DK, 1981.
Ph. Schnoebelen. Decomposable regular languages and the shuffle operator. EATCS Bull., 67:283–289, 1999.
H. Seidl. Finite tree automata with cost function. Theoretical Computer Science, 126(1):113–142, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lugiez, D., Schnoebelen, P. (2000). Decidable First-Order Transition Logics for PA-Processes. In: Montanari, U., Rolim, J.D.P., Welzl, E. (eds) Automata, Languages and Programming. ICALP 2000. Lecture Notes in Computer Science, vol 1853. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45022-X_30
Download citation
DOI: https://doi.org/10.1007/3-540-45022-X_30
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67715-4
Online ISBN: 978-3-540-45022-1
eBook Packages: Springer Book Archive