Journal of Logic, Language and Information 18 (4):465-491 (2009)
|Abstract||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)|
|Through your library||Configure|
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.
P. Blackburn & B. ten Cate (2006). Pure Extensions, Proof Rules, and Hybrid Axiomatics. Studia Logica 84 (2):277 - 322.
Torben BraÜner (2005). Natural Deduction for First-Order Hybrid Logic. Journal of Logic, Language and Information 14 (2):173-198.
Patrick Blackburn & Maarten Marx (2003). Constructive Interpolation in Hybrid Logic. Journal of Symbolic Logic 68 (2):463-480.
Nicola Angius & Guglielmo Tamburrini (2011). Scientific Theories of Computational Systems in Model Checking. Minds and Machines 21 (2):323-336.
M. Kacprzak & W. Penczek (2004). A Sat-Based Approach to Unbounded Model Checking for Alternating-Time Temporal Epistemic Logic. Synthese 142 (2):203 - 227.
Dietmar Berwanger (2003). Game Logic is Strong Enough for Parity Games. Studia Logica 75 (2):205 - 219.
Natasha Alechina & Brian Logan (2009). A Logic of Situated Resource-Bounded Agents. Journal of Logic, Language and Information 18 (1):79-95.
Stephan Merz (2002). Model Checking Techniqes for the Analysis of Reactive Systems. Synthese 133 (1-2):173 - 201.
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 downloads13 ( #95,504 of 722,826 )
Recent downloads (6 months)1 ( #60,541 of 722,826 )
How can I increase my downloads?