David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Journal of Logic, Language and Information 18 (4):465-491 (2009)
We consider the model checking problem for Hybrid Logic. Known algorithms so far are global in the sense that they compute, inductively, in every step the set of all worlds of a Kripke structure that satisfy a subformula of the input. Hence, they always exploit the entire structure. Local model checking tries to avoid this by only traversing necessary parts of the input in order to establish or refute the satisfaction relation between a given world and a formula. We present a framework for local model checking of Hybrid Logic based on games. We show that these games are simple reachability games for ordinary Hybrid Logic and weak Büchi games for Hybrid Logic with operators interpreted over the transitive closure of the accessibility relation of the underlying Kripke frame, and show how to solve these games thus solving the local model checking problem. Since the first-order part of Hybrid Logic is inherently hard to localise in model checking, we give examples, in the end, of how global model checkers can be optimised in certain special cases using well-established techniques like fixpoint approximations and divide-and-conquer algorithms.
|Keywords||Local model checking Büchi games|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
Nicole Bidoit, Serenella Cerrito & Virginie Thion (2004). A First Step Towardsmodeling Semistructured Data in Hybrid Multimodal Logic. Journal of Applied Non-Classical Logics 14 (4):447-475.
R. A. Bull (1970). An Approach to Tense Logic. Theoria 36 (3):282-300.
Valentin Goranko (1996). Hierarchies of Modal and Temporal Logics with Reference Pointers. Journal of Logic, Language and Information 5 (1):1-24.
Citations of this work BETA
No citations found.
Similar books and articles
Mark Kaminski & Gert Smolka (2009). Terminating Tableau Systems for Hybrid Logic with Difference and Converse. Journal of Logic, Language and Information 18 (4):437-464.
Stephan Merz (2002). Model Checking Techniqes for the Analysis of Reactive Systems. Synthese 133 (1-2):173 - 201.
Natasha Alechina & Brian Logan (2009). A Logic of Situated Resource-Bounded Agents. Journal of Logic, Language and Information 18 (1):79-95.
Dietmar Berwanger (2003). Game Logic is Strong Enough for Parity Games. Studia Logica 75 (2):205 - 219.
M. Kacprzak & W. Penczek (2004). A Sat-Based Approach to Unbounded Model Checking for Alternating-Time Temporal Epistemic Logic. Synthese 142 (2):203 - 227.
Nicola Angius & Guglielmo Tamburrini (2011). Scientific Theories of Computational Systems in Model Checking. Minds and Machines 21 (2):323-336.
Patrick Blackburn & Maarten Marx (2003). Constructive Interpolation in Hybrid Logic. Journal of Symbolic Logic 68 (2):463-480.
Torben BraÜner (2005). Natural Deduction for First-Order Hybrid Logic. Journal of Logic, Language and Information 14 (2):173-198.
P. Blackburn & B. ten Cate (2006). Pure Extensions, Proof Rules, and Hybrid Axiomatics. Studia Logica 84 (2):277 - 322.
Martin Mundhenk & Thomas Schneider (2009). The Complexity of Hybrid Logics Over Equivalence Relations. Journal of Logic, Language and Information 18 (4):493-514.
Added to index2009-04-27
Total downloads20 ( #118,998 of 1,696,233 )
Recent downloads (6 months)4 ( #138,000 of 1,696,233 )
How can I increase my downloads?