Сибирский федеральный университет

Тип публикации: статья из журнала (материалы конференций, опубликованные в журналах)

Год издания: 2008

Идентификатор DOI: 10.1007/978-3-540-69407-6_4

Ключевые слова: Decidability algorithms, Hybrid logics, Linear temporal logic, Multi-agent logics, Relational Kripke-Hintikka models, Satisfiability, Agents, Boolean functions, Communication channels (information theory), Computability and decidability, Eigenvalues and eigenfunctions, Fuzzy logic, Information theory, Knowledge based systems, Recursive functions, Stabilizers (agents), (+ mod 2N) operation, (e ,2e) theory, Common knowledge, decidability problems, Heidelberg (CO), Linear Temporal Logic (LTL), Multi agents, Reduced forms, Satisfiability (SAT) problems, Springer (CO), Time points, Temporal logic

Аннотация: Our paper considers a hybrid between the multi-agent logic with the local common knowledge operation and an extended version of the linear temporal logic . The logic is based on the semantics of Kripe/Hintikka models with potentially infinite runs and the time points represented by clusters of states with agents' accessibility relations. We study the satisfiability problem for and related decidability problem. The key result is an algorithm which recognizes theorems of (so we show that is decidable), which, as a consequence, also solves the satisfiability problem. Technique is based on verification of validity for special normal reduced forms of rules in models of double exponential in the size of rules. © 2008 Springer-Verlag Berlin Heidelberg.

Журнал: (15 June 2008 through 20 June 2008, Athens

Выпуск журнала: Vol. 5028 LNCS

Номера страниц: 32-41

• Rybakov V. (Manchester Metropolitan University)
• Babenyshev S. (Siberian Federal University)

• Scopus
• Web of Science Core Collection
• Ядро РИНЦ (eLIBRARY.RU)