Relative Nondeterministic Information Logic is EXPTIME-complete

We define a relative version of the logic NIL introduced by Orłowska, Pawlak and Vakarelov and we show that satisfiability is not only decidable but also EXPTIME-complete. Such a logic combines two ingredients that are seldom present simultaneously in information logics: frame conditions involving more than one information relation and relative frames. The EXPTIME upper bound is obtained by designing a well-suited decision procedure based on the nonemptiness problem of B¨uchi automata on infinite trees. The paper provides evidence that B¨uchi automata on infinite trees are crucial language acceptors even for relative information logics with multiple types of relations.

• Type: Journal
• Year: 2007
• Where: FUIN
• Authors: Stéphane Demri, Ewa Orlowska
• Keywords: B¨uchi Automata, FUIN 2007, Information Logics, Logics