Model Checking Multi-Agent Systems Against Epistemic Hs Specifications With Regular Expressions
KR'16: Proceedings of the Fifteenth International Conference on Principles of Knowledge Representation and Reasoning(2016)
摘要
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+.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络