Computability in Europe 2008
Logic and Theory of Algorithms

Print current page  Print this page

Regular Talk:
Decidability of Hybrid Logic with Local Common Knowledge based on Linear Temporal Logic LTL

Edit abstract data

Author(s): Vladimir Rybakov and Sergei Babyonyshev
Slot: Wed, 16:50-17:10, Room 22 (col. 4)


Our paper considers a hybrid  LTL_ACK of the multi-agent logic
with the local common knowledge operation and an  extended version
of the linear temporal logic LTL. The logic is based on semantics with
Kripe/Hintikka models on potentially infinite
runs with time points represented by clusters of states with
distributed knowledge of the agents. We study  the satisfiability
problem and decidability of the logic LTL_ACK. Key result is found
algorithm which recognizes theorems of LTL_ACK (so we show that
LTL_ACK is decidable). Technique  is based on verification of
validity of special normal reduced forms of rules in models of
double exponential size in the testing rules.

websites: Arnold Beckmann 2008-05-19 Valid HTML 4.01! Valid CSS!