AAAI Publications, Fifteenth International Conference on the Principles of Knowledge Representation and Reasoning

Font Size: 
Model Checking Multi-Agent Systems against Epistemic HS Specifications with Regular Expressions
Alessio Lomuscio, Jakub Michaliszyn

Last modified: 2016-03-30


We introduce EHS*, a novel temporal-epistemic logic defined on temporal intervals characterised by regular expressions. We investigate the complexity of verifying multi-agent systems against EHS* specifications for a number of fragments of EHS* with results ranging from PSPACE-completeness to non-elementary time. The findings show that, at least for the fragments under analysis, the increase in expressiveness obtained by using regular expressions rather than end-points as standard, can be achieved without increasing the complexity of the problem. We show that the expressiveness of regular expressions can also be adopted at the level of specifications without severe computational cost. To do so we introduce a further temporal-epistemic logic, called EHSre, in which regular expressions are used within propositions, and give a polynomial time reduction of the model checking problem from EHSre to EHS*.


temporal-epistemic logic; model checking; verification

Full Text: PDF