Logic Journal of IGPL Advance Access originally published online on August 12, 2009
Logic Journal of IGPL 2009 17(5):559-587; doi:10.1093/jigpal/jzp021
This article appears in the following Logic Journal of the IGPL issue: Special Issue: Logical and Semantical Frameworks with Applications [View the issue table of contents]
Using modal logics to express and check global graph properties
Computer Science Department and Systems and Computer Engineering Program, Federal University of Rio de Janeiro, Brazil.
E-mail: mario{at}cos.ufrj.br
Systems and Computer Engineering Program, Federal University of Rio de Janeiro, Brazil.
E-mail: luis{at}cos.ufrj.br
Graphs are among the most frequently used structures in Computer Science. Some of the properties that must be checked in many applications are connectivity, acyclicity and the Eulerian and Hamiltonian properties. In this work, we analyze how we can express these four properties with modal logics. This involves two issues: whether each of the modal languages under consideration has enough expressive power to describe these properties and how complex (computationally) it is to use these logics to actually test whether a given graph has some desired property. First, we show that these properties are not definable in a basic modal logic or in any bisimulation-invariant extension of it, like the modal µ-calculus. We then show that it is possible to express some of the above properties in a basic hybrid logic. Unfortunately, the Hamiltonian and Eulerian properties still cannot be efficiently checked. In a second attempt, we propose an extension of CTL* with nominals and show that the Hamiltonian property can be more efficiently checked in this logic than in the previous one. In a third attempt, we extend the basic hybrid logic with the 
operator and show that we can check the Hamiltonian property with optimal (NP) complexity in this logic. Finally, we tackle the Eulerian property in two different ways. First, we develop a generic method to express edge-related properties in hybrid logics and use it to express the Eulerian property. Second, we express a necessary and sufficient condition for the Eulerian property to hold using a graded modal logic.
Key Words: Computational Complexity • Frame-Checking • Graphs • Modal Logic • Model-Checking
Received for publication 22 May 2009.
References
-
[1] Areces C, Blackburn P, Marx M. A road-map on complexity for hybrid logics. (1999) Springer. 307–321. In 8th Annual Conference of the EACSL, volume 1683 of LNCS.
[2] Areces C, Blackburn P, Marx M. The computational complexity of hybrid temporal logics. Logic Journal of the IGPL (2000) 8:653–679.[CrossRef]
[3] Areces C, ten Cate B. Hybrid logics. In: Handbook of Modal Logic—Blackburn P, van Benthem J, Wolter F, eds. (2006) Elsevier. 821–868.
[4] Armando A, Carbone R, Compagna L. LTL model checking for security protocols. (2007) IEEE. 385–396. In 20th IEEE Computer Security Foundations Symposium.
[5] Baltazar P, Chadha R, Mateus P. Quantum computation tree logic – model checking and complete calculus. International Journal of Quantum Information (2008) 6(2):219–236.[CrossRef][Web of Science]
[6] Barbosa VC. An Introduction to Distributed Algorithms (1996) MIT Press.
[7] Benevides MRF. Modal logics for finite graphs. In: Logic for Synchronization and Concurrency—Queiroz R, ed. (2003) Kluwer Academic Publisher. 239–267. Trends in Logic.
[8] Blackburn P, de Rijke M, Venema Y. Modal Logic (2001) Cambridge University Press. Theoretical Tracts in Computer Science.
[9] Bondy JA, Murty USR. Graph Theory with Applications (1979) New York: Elsevier.
[10] Bradfield J, Stirling C. Modal mu calculi. In: Handbook of Modal Logic—Blackburn P, van Benthem J, Wolter F, eds. (2006) Elsevier. 721–756.
[11] Clarke EM, Grumberg O, Peled D. Model Checking (2000) MIT Press.
[12] Dam M. CTL* and ECTL* as fragments of the modal mu-calculus. Theoretical Computer Science (1994) 126:77–96.[CrossRef][Web of Science]
[13] Emerson EA. Temporal and modal logic. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics—van Leeuwen J, ed. (1990) North-Holland Pub. Co./MIT Press. 995–1072.
[14] Ferrante A, Napoli M, Parente M. CTL model-checking with graded quantifiers. (2008) Springer. 18–32. In 6th International Symposium on Automated Technology for Verification and Analysis, volume 5311 of LNCS.
[15] Fine K. In so many possible worlds. Notre Dame Journal of Formal Logic (1972) 13(4):516–520.[CrossRef]
[16] Franceschet M, de Rijke M. Model checking hybrid logics (with an application to semistructured data). Journal of Applied Logic (2006) 4(3):279–304.[CrossRef]
[17] Gay SJ, Nagarajan R, Papanikolaou N. Model-checking quantum protocols. http://www.dcs.warwick.ac.uk/~nikos/downloads/gnp.pdf.
[18] Karp R. Reducibility among combinatorial problems. In: Complexity of Computer Computations (1972) New York: Plenum. 85–103.
[19] Kovács M, Gönczy L, Varró D. Formal analysis of BPEL workflows with compensation by model checking. In: International Journal of Computer Systems and Engineering. to appear.
[20] Lynch N. Distributed Algorithms (1996) San Mateo: Morgan Kaufmann Publishers.
[21] Moller F, Rabinovich A. On the expressive power of CTL*. (1999) 360–369. In XIV IEEE Symposium on Logic in Computer Science.
[22] Sattler U, Vardi MY. The hybrid µ-calculus. (2001) Springer. 76–91. In First International Joint Conference in Automated Reasoning, volume 2083 of LNAI.
[23] Strecker M. Modeling and verifying graph transformations in proof assistants. In: 4th International Workshop on Computing with Terms and Graphs (2008) Elsevier. 135–148. volume 203 of Electronic Notes in Theoretical Computer Science.
[24] ten Cate B, Franceschet M. On the complexity of hybrid logics with binders. In: 19th International Workshop of Computer Science Logic (2005) Springer. volume 3634 of LNCS, pages 339–354.
[25] van der Hoek W, de Rijke M. Counting objects. Journal of Logic and Computation (1995) 5(3):325–345.
[26] Venema Y. Lectures on the modal mu-calculus. http://staff.science.uva.nl/~yde/teaching/ml/mu/mu.pdf.
CiteULike 
Connotea 
Del.icio.us What's this?
| ||||||||||||||||||||||||||||||||||||||||||||||||