Title: Reasoning about Time-Dependent Multi-agents: Foundations of Theorem Proving and Model Checking
Abstract: Firstly, an extension of linear-time temporal logic (LTL), called an agents-indexed linear-time temporal logic (ALTL), is introduced as a Gentzen-type sequent calculus. ALTL is intended to appropriately express reasoning about time-dependent multi-agents within a proof system. The cut-elimination and completeness theorems for ALTL are shown. Secondly, an extension of computation tree logic (CTL), called an agents-indexed computation tree logic (ACTL), is introduced as a Kripke-type semantics. ACTL is intended to appropriately formalize reasoning about time-dependent multi-agents within an executable temporal logic by model checking. The model-checking, validity and satisfiability problems for ACTL are shown to be decidable.
Publication Year: 2012
Publication Date: 2012-01-01
Language: en
Type: book-chapter
Indexed In: ['crossref']
Access and Citation
Cited By Count: 1
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot