Abstract
This chapter presents the hybrid Temporal Trace Language (TTL) for
formal specification and analysis of dynamic properties of multi-agent
systems. This language supports specification of both qualitative
and quantitative aspects, and subsumes languages based on differential
equations and temporal logics. TTL has a high expressivity and normal
forms that enable automated analysis. Software environments for performing
verification of TTL specifications have been developed. TTL proved
its value in a number of domains.
Users
Please
log in to take part in the discussion (add own reviews or comments).