Using modal logics to express and check global graph properties

Logic Journal of the IGPL 17 (5):559-587 (2009)
  Copy   BIBTEX


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 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 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.



    Upload a copy of this work     Papers currently archived: 86,403

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

On the Beth properties of some intuitionistic modal logics.C. Luppi - 2002 - Archive for Mathematical Logic 41 (5):443-454.
Bisimulation, modal logic and model checking games.C. Stirling - 1999 - Logic Journal of the IGPL 7 (1):103-124.
Prefinitely axiomatizable modal and intermediate logics.Marcus Kracht - 1993 - Mathematical Logic Quarterly 39 (1):301-322.
Abstract modal logics.Ramon Jansana - 1995 - Studia Logica 55 (2):273 - 299.
Modal Hybrid Logic.Andrzej Indrzejczak - 2007 - Logic and Logical Philosophy 16 (2-3):147-257.
The Accidental Properties of Numbers and Properties.Harold Noonan & Mark Jago - 2012 - Thought: A Journal of Philosophy 1 (2):134-140.


Added to PP

18 (#681,920)

6 months
3 (#340,008)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

A logic for diffusion in social networks.Zoé Christoff & Jens Ulrik Hansen - 2015 - Journal of Applied Logic 13 (1):48-77.

Add more citations

References found in this work

In so many possible worlds.Kit Fine - 1972 - Notre Dame Journal of Formal Logic 13 (4):516-520.
Model checking hybrid logics.Massimo Franceschet & Maarten de Rijke - 2006 - Journal of Applied Logic 4 (3):279-304.

Add more references