Demri, Stéphane; Sattler, Ulrike Automata-theoretic decision procedures for information logics. (English) Zbl 1025.03021 Fundam. Inform. 53, No. 1, 1-22 (2002). Summary: 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 properties of information systems, and provides 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. Cited in 1 Document MSC: 03B70 Logic in computer science 03B25 Decidability of theories and sets of sentences 68Q25 Analysis of algorithms and problem complexity 03D05 Automata and formal grammars in connection with logical questions 68Q60 Specification and verification (program logics, model checking, etc.) Keywords:computational complexity; Büchi tree automaton; information logic; hybrid logic PDFBibTeX XMLCite \textit{S. Demri} and \textit{U. Sattler}, Fundam. Inform. 53, No. 1, 1--22 (2002; Zbl 1025.03021)