Abstract
We delimit the boundary between decidability versus undecidability of the weak monadic second-order logic of one successor (WS1S) extended with linear cardinality constraints of the form |X 1|+...+|X r| < |Y 1|+...+|Y s|, where the X is and Y js range over finite subsets of natural numbers. Our decidability and undecidability results are based on an extension of the classic logic-automata connection using a novel automaton model based on Parikh maps.
This work was supported by SRI International internal research and development, and NASA through contract NAS1-00079.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
D. Basin and S. Friedrich, Combining WS1S and HOL, in FroCos’98, Applied Logic Series, 2000, pp. 39–56.
D. Basin, S. Friedrich, and S. Mödersheim, B2M: A semantic based tool for BLIF hardware descriptions, in FMCAD’00, vol. 1954 of LNCS, 2000, pp. 91–107.
D. Basin and N. Klarlund, Automata based symbolic reasoning in hardware verification, FMSD, 13 (1998), pp. 255–288.
H. Comon and Y. Jurski, Multiple counters automata, safety analysis and Pres-burger arithmetic, in CAV’98, vol. 1427 of LNCS, 1998, pp. 268–279.
S. Dal Zilio and D. Lugiez, XML schema, tree logic and sheaves automata, Research Report 4631, INRIA, 2002.
J. Dassow and V. Mitrana, Finite automata over free groups, International Journal of Algebra and Computation, 10 (2000), pp. 725–737.
A. Finkel and G. Sutre, Decidability of rechability problems for classes of two counter automata, in STACS’00, vol. 1770 of LNCS, 2000, pp. 346–357.
M. Gordon, Why higher-order logics is a good formalism for specifying and verifying hardware, in Formal Aspects of VLSI Design, North-Holland, 1986, pp. 153–177.
G. Gottlob and C. Koch, Monadic Datalog and the expressive power of languages for web information extraction, in PODS’02, 2002, pp. 17–28.
J. Henriksen, J. Jensen, M. Jorgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm, Mona: Monadic second-order logic in practice, in TACAS’95, vol. 1019 of LNCS, 1995, pp. 89–110.
O. Ibarra, Reversal-bounded multicounter machines and their decision problems, JACM, 25 (1978), pp. 116–133.
O. Ibarra, J. Su, Z. Dang, T. Bultan, and R. Kemmerer, Counter machines and verification problems, TCS, 289 (2002), pp. 165–189.
F. Klaedtke, CMona: Monadic second-order logics with linear cardinality constraints in practice. in preparation, 2003.
F. Klaedtke and H. Rueß, WS1S with cardinality constraints, Technical Report SRI-CSL-05-01, SRI International, 2001.
—, Parikh automata and monadic second-order logics with linear cardinality constraints, Technical Report 177, Albert-Ludwigs-Universität Freiburg, 2002. (revised version).
N. Klarlund, A. Møller, and M. Schwartzbach, MONA implementation secrets, in CIAA’00, vol. 2088 of LNCS, 2000, pp. 182–194.
N. Klarlund, M. Nielsen, and K. Sunesen, Automated logical verification based on trace abstraction, in PODC’96, 1996, pp. 101–110.
L. Lamport, R. Shostak, and M. Pease, The Byzantine Generals problem, TOPLAS, 4 (1982), pp. 382–401.
A. Meyer, Weak monadic second-order theory of successor is not elementary-recursive, in Logic Colloquium, vol. 453 of LNM, 1975, pp. 132–154.
V. Mitrana and R. Stiebe, Extended finite automata over groups, Discrete Applied Mathematics, 108 (2001), pp. 287–300.
S. Owre and H. Ruess, Integrating WS1S with PVS, in CAV’00, vol. 1855 of LNCS, 2000, pp. 548–551.
M. Parigot and E. Pelz, A logical approach of Petri net languages, TCS, 39 (1985), pp. 155–169.
R. Parikh, On context-free languages, JACM, 13 (1966), pp. 570–581.
J. Rushby, Systematic formal verification for fault-tolerant time-triggered algorithms, IEEE Trans. on Software Engineering, 2 (1999), pp. 651–660.
M. Smith and N. Klarlund, Verification of a sliding window protocol using IOA and MONA, in FORTE/PSTV’00, vol. 183 of IFIP Conf. Proc., 2000, pp. 19–34.
L. Stockmeyer, The Complexity of Decision Problems in Automata Theory and Logic, PhD thesis, Dept. of Electrical Engineering, MIT, Boston, Mass., 1974.
W. Thomas, Languages, automata, and logic, in Handbook of Formal Languages, vol. 3, Springer-Verlag, 1997, pp. 389–455.
A. Wilk and A. Pnueli, Specification and verification of VLSI systems, in IC-CAD’89, 1989, pp. 460–463.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Klaedtke, F., Rueß, H. (2003). Monadic Second-Order Logics with Cardinalities. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds) Automata, Languages and Programming. ICALP 2003. Lecture Notes in Computer Science, vol 2719. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45061-0_54
Download citation
DOI: https://doi.org/10.1007/3-540-45061-0_54
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40493-4
Online ISBN: 978-3-540-45061-0
eBook Packages: Springer Book Archive