English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Timed Automata (TA) is de facto a standard modelling formalism to representsystems when the interest is the analysis of their behaviour as timeprogresses. This modelling formalism is mostly used for checking whether thebehaviours of a system satisfy a set of properties of interest. Even ifefficient model-checkers for Timed Automata exist, these tools are not easilyconfigurable. First, they are not designed to easily allow adding new TimedAutomata constructs, such as new synchronization mechanisms or communicationprocedures, but they assume a fixed set of Timed Automata constructs. Second,they usually do not support the full Metric Interval Temporal Logic (MITL) andrely on a precise semantics for the logic in which the property of interest isspecified which cannot be easily modified and customized. Finally, they do noteasily allow using different solvers that may speed up verification indifferent contexts. This paper presents a novel technique to perform modelchecking of full Metric Interval Temporal Logic (MITL) properties on TA. Thetechnique relies on the translation of both the TA and the MITL formula into anintermediate Constraint LTL over clocks (CLTLoc) formula which is verifiedthrough an available decision procedure. The technique is flexible since theintermediate logic allows the encoding of new semantics as well as new TAconstructs, by just adding new CLTLoc formulae. Furthermore, our technique isnot bound to a specific solver as the intermediate CLTLoc formula can beverified using different procedures.

Verifying MITL formulae on Timed Automata considering a Continuous Time Semantics