Mona: Monadic second-order logic in practice
- 453 Downloads
The purpose of this article is to introduce Monadic Second-order Logic as a practical means of specifying regularity. The logic is a highly succinct alternative to the use of regular expressions. We have built a tool MONA, which acts as a decision procedure and as a translator to finite-state automata. The tool is based on new algorithms for minimizing finite-state automata that use binary decision diagrams (BDDs) to represent transition functions in compressed form. A byproduct of this work is an algorithm that matches the time but improves the space of Sieling and Wegener's algorithm to reduce OBDDs in linear time.
The potential applications are numerous. We discuss text processing, Boolean circuits, and distributed systems. Our main example is an automatic proof of properties for the “Dining Philosophers with Encyclopedia” example by Kurshan and MacMillan. We establish these properties for the parameterized case without the use of induction.
Our results show that, contrary to common beliefs, high computational complexity may be a desired feature of a specification formalism.
KeywordsBoolean Function Regular Expression Transition Relation Regular Language Decision Node
- [AHU74]A. Aho, J. Hopcroft, and J. Ullman. Design and Analysis of Computer Algorithms. Addison-Wesley, 1974.Google Scholar
- [BK95]D. Basin and N. Klarlund. Hardware verification using monadic second-order logic. Technical Report RS-96-7, BRICS, 1995. To appear in CAV '95 Proceedings.Google Scholar
- [Bry86]R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, Aug 1986.Google Scholar
- [Bry92]R. E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing surveys, 24(3):293–318, September 1992.Google Scholar
- [BSV93]F. Balarin and A.L. Sangiovanni-Vincentelli. An iterative approach to language containment. In Computer Aided Verification, CAV '93, LNCS 697, pages 29–40, 1993.Google Scholar
- [CP94]J. Cai and R. Paige. Using multiset discrimination to solve language processing problems without hashing. to appear Theoretical Computer Science, 1994. also, U. of Copenhagen Tech. Report, DIKU-TR Num. D-209, 94/16, URL ftp://ftp.diku.dk/diku/semantics/papers/D-209.ps.z.Google Scholar
- [CR94]M-M Corsini and A. Rauzy. Symbolic model checking and constraint logic programming: a cross-fertilisation. In 5th. Europ. Symp. on Programming, LNCS 788, pages 180–194, 1994.Google Scholar
- [GF93]A. Gupta and A.L. Fisher. Parametric circuit representation using inductive boolean functions. In Computer Aided Verification, CAV '93, LNCS 697, pages 15–28, 1993.Google Scholar
- [Hop71]J. Hopcroft. An n log n algorithm for minimizing states in a finite automaton. In Z. Kohavi and Paz A., editors, Theory of machines and computations, pages 189–196. Academic Press, 1971.Google Scholar
- [JJK94]J. Jensen, M. Jørgensen, and N. Klarlund. Monadic second-order logic for parameterized verification. Technical report, BRICS Report Series RS-94-10, Department of Computer Science, University of Aarhus, 1994.Google Scholar
- [KM89]B. Kurshan and K. McMillan. A structural induction theorem for processes. In Proc. Eigth Symp. Princ. of Distributed Computing, pages 239–247, 1989.Google Scholar
- [PT87]R. Paige and R. Tarjan. Three efficient algorithms based on partition refinement. SIAM Journal of Computing, 16(6), 1987.Google Scholar
- [Rev92]D. Revuz. Minimisation of acyclic deterministic automata in linear time. Theoretical Computer Science, 92(1):181–189, 1992.Google Scholar
- [RS93]J-K. Rho and F. Somenzi. Automatic generation of network invariants for the verification of iterative sequential systems. In Computer Aided Verification, CAV '93, LNCS 697, pages 123–137, 1993.Google Scholar
- [Ste93]M. Steinmann. Übersetzung von logischen Ausdrücken in Baumautomaten: Entwicklung eines Verfahrens und seine Implementierung. Unpublished, 1993.Google Scholar
- [SW93]D. Sieling and I. Wegener. Reduction of OBDDs in linear time. IPL, 48:139–144, 1993.Google Scholar
- [Tho90]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.Google Scholar