In a former work, we have presented/implemented a framework for modeling and verifying multi-agent systems, using hybrid automata. To specify properties of those systems, one needs a specification language that brings, at the same level of specification, both the qualitative and quantitative requirements. For this aim, there have been proposed several temporal logics with either event or state based approach. Both approaches have their pros and cons which should not be played off against each other. This paper contributes to present a variant of temporal logics which combines the expressiveness of both approaches. Using this proposed logic, we are able reason about many properties in a concise and intuitive manner. In particular, we concentrate on those types of properties that can be verified using reachability analysis. Hence these properties can be verified directly within our implemented framework.
展开▼
