Skip Navigation


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
Right arrow Full Text (PDF)
Right arrow All Versions of this Article:
17/5/559    most recent
jzp021v1
Right arrow References
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Benevides, M. R. F.
Right arrow Articles by Schechter, L. M.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author 2009. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

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

Mario R. F. Benevides

Computer Science Department and Systems and Computer Engineering Program, Federal University of Rio de Janeiro, Brazil.
E-mail: mario{at}cos.ufrj.br

L. Menasché Schechter

Systems and Computer Engineering Program, Federal University of Rio de Janeiro, Brazil.
E-mail: luis{at}cos.ufrj.br


  Abstract

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 {downarrow} 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.
Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer: Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.