Abstract
The satisfiability checking problem is known to be decidable for a variety of modal/temporal logics such as the modal μ-calculus, but effective implementation has not necessarily been developed for all such logics. In this paper, we propose a decision procedure using the tableau method for the alternation-free two-way modal μ-calculus. Although the size of the tableau set maintained in the method might be large for complex formulas, the set and the operations on it can be expressed using BDD and therefore we can implement the method in an effective way.
This research was supported by Core Research for Evolutional Science and Technology (CREST) Program “New High-performance Information Processing Technology Supporting Information-oriented Society” of Japan Science and Technology Agency (JST).
This research was partially supported by the Ministry of Education, Science, Sports and Culture, Grant-in-Aid for Scientific Research on Priority Areas, 16016211, 2004.
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
Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24(3), 293–318 (1992)
Emerson, E.A., Clarke, E.M.: Using branching-time temporal logic to synthesize synchronization skeletons. Science of Computer Programming 2(3), 241–266 (1982)
Grädel, E.: Guarded fixed point logics and the monadic theory of countable trees. Theoretical Computer Science 288, 129–152 (2002)
Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research. LNCS, vol. 2500. Springer, Heidelberg (2002)
Hagiya, M., Takahashi, K., Yamamoto, M., Sato, T.: Analysis of synchronous and asynchronous cellular automata using abstraction by temporal logic. In: Kameyama, Y., Stuckey, P.J. (eds.) FLOPS 2004, vol. 2998, pp. 7–21. Springer, Heidelberg (2004)
Henriksen, J.G., Jensen, J.L., Jørgensen, M.E., Klarlund, N., Paige, R., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995, vol. 1019, pp. 89–110. Springer, Heidelberg (1995)
JavaBDD, http://javabdd.sourceforge.net/
Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)
Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. ACM Transactions on Programming Languages and Systems 6(1), 68–93 (1984)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publ., Dordrecht (1993)
Niwinski, D., Walukiewicz, I.: Games for the μ-calculus. Theoretical Computer Science 163(1,2), 99–116 (1996)
Pan, G., Sattler, U., Vardi, M.Y.: BDD-based decision procedures for K. In: Voronkov, A. (ed.) CADE 2002. LNCS, vol. 2392, pp. 16–30. Springer, Heidelberg (2002)
Pan, G., Vardi, M.Y.: Optimizing a BDD-based modal solver. In: Baader, F. (ed.) CADE 2003. LNCS, vol. 2741, pp. 75–89. Springer, Heidelberg (2003)
Safra, S.: On the complexity of omega-automata. In: Proceedings of the 29th Annual Symposium on Foundations of Computer Science, FoCS 1988, pp. 319–327. IEEE Computer Society Press, Los Alamitos (1988)
Takahashi, K., Hagiya, M.: Abstraction of graph transformation using temporal formulas. In: Supplemental Volume of the 2003 International Conference on Dependable Systems and Networks (DSN 2003), pp. W–65–W–66 (2003)
Tozawa, A.: On binary tree logic for XML and its satisifiability test. In: Sixth Workshop on Programming and Programming Language, PPL 2004 (2004)
Tozawa, A., Tanabe, Y., Hagiya, M.: Experiments on global type checking and termination checking for XML transducer. IBM Research Report RT0614 (2005)
Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998, vol. 1443, pp. 628–641. Springer, Heidelberg (1998)
Yamamoto, M., Tanabe, Y., Takahashi, K., Hagiya, M.: Abstraction of graph transformation systems by temporal logic and its verification. In: IFIP Working Conference on Verified Software: Tools, Techniques, and Experiments (to appear)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tanabe, Y., Takahashi, K., Yamamoto, M., Tozawa, A., Hagiya, M. (2005). A Decision Procedure for the Alternation-Free Two-Way Modal μ-Calculus . In: Beckert, B. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2005. Lecture Notes in Computer Science(), vol 3702. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11554554_21
Download citation
DOI: https://doi.org/10.1007/11554554_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28931-9
Online ISBN: 978-3-540-31822-4
eBook Packages: Computer ScienceComputer Science (R0)