Automata-Theoretic Decision Procedures for Information Logics

Automata-theoretic decision procedures for solving model-checking and satisfiability problems for temporal, dynamic, and description logics have flourished during the past decades. In the paper we define an EXPTIME decision procedure based on the emptiness problem of Büchi automata on infinite trees for the very expressive information logic SIM designed for reasoning about information systems. This logic involves modal parameters satisfying certain properties to capture the relevant nominals at the formula level, Boolean expressions and nominals at the modal level, an implicit intersection operation for relations, and a universal modality. The original combination of known techniques allows us to solve the open question related to the EXPTIME-completeness of SIM. Furthermore, we discuss how variants of SIM can be treated similarly although the decidability status of some of them is still unknown.

• Publication year

  2002

• Venue

  Fundamenta Informaticae

• Publication date

  2002-01-01

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.3233/FUN-2002-53101
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• The Complexity of the Graded µ-Calculus

  2002cited by this paper
• Description logics: foundations for class-based knowledge representation

  2002cited by this paper
• Incomplete Information: Structure, Inference, Complexity

  2002cited by this paper
• The Complexity of Reasoning with Boolean Modal Logics

  2001cited by this paper
• Why are Modal Logics so Robustly Decidable?

  2001cited by this paper
• On model checking for the µ-calculus and its fragments

  2001cited by this paper
• The Hybrid mu-Calculus

  2001influential reference
• Internalization: The Case of Hybrid Logics

  2001cited by this paper
• The Hybrid µ-Calculus

  2001cited by this paper
• On Modal Logics Characterized by Models with Relative Accessibility Relations: Part II

  2000cited by this paper
• An automata-theoretic approach to branching-time model checking

  2000cited by this paper
• Internalizing labelled deduction

  2000cited by this paper
• Representation, Reasoning, and Relational Structures: a Hybrid Logic Manifesto

  2000cited by this paper
• On Modal Logics Characterized by Models with Relative Accessibility Relations: Part I

  2000cited by this paper
• A Logic with Relative Knowledge Operators

  1999cited by this paper
• Sequent Calculi for Nominal Tense Logics: A Step Towards Mechanization?

  1999cited by this paper
• Tableau Calculi for Hybrid Logics

  1999cited by this paper
• Reasoning in Expressive Description Logics with Fixpoints based on Automata on Infinite Trees

  1999cited by this paper
• A Logic for Reasoning about Similarity

  1998influential reference
• Rough Relations and Logics

  1998cited by this paper
• Relative Similarity Logics are Decidable: Reduction to FO2 with Equality

  1998cited by this paper
• Reasoning about The Past with Two-Way Automata

  1998cited by this paper
• Rough Sets in Knowledge Discovery 2

  1998cited by this paper
• The Model Checker SPIN

  1997cited by this paper
• On the Decision Problem for Two-Variable First-Order Logic

  1997cited by this paper
• Incomplete Information: Rough Set Analysis

  1997cited by this paper
• Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics

  1997cited by this paper
• A Logic for Reasoning about Relative Similarity

  1997cited by this paper
• The Price of Universality

  1996cited by this paper
• Modal Logics with Relative Accessibility Relations

  1996cited by this paper
• The Complexity of Propositional Modal Theories and the Complexity of Consistency of Propositional Modal Theories

  1994cited by this paper
• Reasoning About Infinite Computations

  1994cited by this paper
• Reasoning about In nite Computations

  1994cited by this paper
• A model logic for similarity relations in pawlak knowledge representation systems

  1991cited by this paper
• On a Decision Method in Restricted Second Order Arithmetic

  1990cited by this paper
• A Note on Boolean Modal Logic

  1990cited by this paper
• An Automata Theoretic Decision Procedure for the Propositional Mu-Calculus

  1989cited by this paper
• Modal Logics for Knowledge Representation Systems

  1989cited by this paper
• The complexity of tree automata and logics of programs

  1988cited by this paper
• Abstract Characterization of some Knowledge Representation Systems and the Logic NIL of Nondeterministic Information

  1986cited by this paper
• Automata theoretic techniques for modal logics of programs: (Extended abstract)

  1984cited by this paper
• Expressive Power of Knowledge Representation Systems

  1984cited by this paper
• Weakly Definable Relations and Special Automata

  1970cited by this paper
• Decidability of second-order theories and automata on infinite trees

  1968cited by this paper
• On a decision method in restricted second-order arithmetic

  1960cited by this paper
• INFORMATION SYSTEMS THEORETICAL FOUNDATIONS

  year unknowncited by this paper

• Robustness of Constraint Automata for Description Logics with Concrete Domains

  2026influential citation
• Compositional Verification of Business Processes by Model-Checking

  2010cites this paper
• Deciding Second-order Logics using Database Evaluation Techniques

  2008cites this paper
• Deciding Second-order Logics using Database Evaluation Techniques

  2008cites this paper
• Logics of similarity and their dual tableaux. A survey

  2008cites this paper
• Relative Nondeterministic Information Logic is EXPTIME-complete

  2007influential citation
• An Incremental Technique for Automata-Based Decision Procedures

  2007cites this paper
• Rudiments of rough sets

  2007cites this paper
• Description Logics for Ontologies

  2003cites this paper