Model checking multi-agent systems against epistemic HS specifications with regular expressions

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