Abstract
In this note, we describe how a fragment of arithmetic can be decided in practice. We follow essentially the ideas of [8], which we have embedded in the Mona tool.
Mona is an implementation of Monadic Secondorder Logic on finite strings (and trees). The previous semantics used in Mona is the one provided in current literature [7, 9], where the meaning of first-order terms is restricted to being a position in the string over which the formula is interpreted.
In this note, we describe our new semantics, where terms are interpreted relative to all natural numbers. With this semantics Mona becomes a decision procedure for the calculus called WS1S, the Weak Second-order theory of 1 Successor.
We also show how the Mona representation of automata subsumes a recent proposal for representing queues. We exploit the natural semantics to carry out automated reasoning about queue operations.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
D. Basin and N. Klarlund. Hardware verification using monadic second-order logic. In Computer aided verification: 7th International Conference, CAV '95, LNCS 939, 1995.
P. Godefroid and D.E. Long. Symbolic protocol verification with Queue BDDs. In Proc. LICS' 96, 1996.
J.G. Henriksen, J. Jensen, M. Jørgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS '95, LNCS 1019, 1996. Also available through http://www.brics.aau.dk/klarlund.
N. Klarlund, J. Koistinen, and M. Schwartzbach. Formal design constraints. In Proc. OOPSLA '96, 1996. to appear.
N. Klarlund, M. Nielsen, and K. Sunesen. Automated logical verification based on trace abstraction. Technical Report RS-95-53, BRICS, 1995. To appear in Proceedings of PODC '96.
N. Klarlund, M. Nielsen, and K. Sunesen. A case study in automated verification based on trace abstractions. Technical Report RS-96-?, BRICS, Aarhus University, 1996. In preparation. To appear in LNCS proceedings on Dagstuhl workshop.
Howard Straubing. Finite Automata, Formal Logic, and Circuit Complexity. Birkhäuser, 1994.
J.W. Thatcher and J.B. Wright. Generalized finite automata with an application to a decision problem of second-order logic. Math. Systems Theory, 2:57–82, 1968.
W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 133–191. MIT Press/Elsevier, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Biehl, M., Klarlund, N., Rauhe, T. (1996). Mona: Decidable arithmetic in practice. In: Jonsson, B., Parrow, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 1996. Lecture Notes in Computer Science, vol 1135. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61648-9_56
Download citation
DOI: https://doi.org/10.1007/3-540-61648-9_56
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61648-1
Online ISBN: 978-3-540-70653-3
eBook Packages: Springer Book Archive