Implementation of Epistemic Operators for Model Checking Multi-agent Systems (CROSBI ID 155890)
Prilog u časopisu | izvorni znanstveni rad | međunarodna recenzija
Podaci o odgovornosti
Bagić Babac, Marina ; Kunštić, Marijan
engleski
Implementation of Epistemic Operators for Model Checking Multi-agent Systems
The problem of multi-agent system (MAS) specification and verification has been introduced in this paper, Epistemic transition system (ETS) represents an agent as the smallest unit in a multi-agent system, while Epistemic synchronous product (ESP) represents the formal model for a multi-agent system. Therefore, a formal framework for epistemic properties of multi-agent systems has been provided. A special extension of Action computation tree logic with unless operator for epistemic reasoning (ACTLW-ER) is used for MAS model checking. Epistemic operators of ACTLW-ER are implemented by symbolic model checking algorithms using binary decision diagrams.
Action Computation Tree Logic with Unless Operator; Epistemic Reasoning; Multi-agent Systems
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano