Skip to main content.

This page’s menu:

Introduction

About UPPAAL CORA

UPPAAL CORA is a branch of UPPAAL for Cost Optimal Reachability Anslysis developed by the UPPAAL team as part of the VHS and AMETIST projects. Whereas UPPAAL uses timed automata as its modelling language, UPPAAL CORA uses linearly priced timed automata (LPTA). Given an LPTA model, UPPAAL CORA finds the optimal paths to a state satisfying some goal conditions. Optimal here means the path with the lowest accumulated cost.

UPPAAL CORA provides a number of extensions to the modelling language of UPPAAL, that allows the user to convey additional insight about the model to the tool, which in turn can improve the performance of UPPAAL CORA. In particular, it is possible to annotate the model with an estimate of the remaining cost for reaching a state satisfying the goal conditions. This can significantly reduce the time required for finding a good or an optimal solution.

About the Language

UPPAAL CORA uses the LPTA modelling languages. "So what is an LPTA?", you ask. Let us start with a timed automaton. A timed automaton is basically a finite state machine extended with a set of non-negative real valued variables called clocks. These variables are incremented synchronously with the passage of time. E.g. if 2.3 time units pass, then all clocks are incremented by 2.3. It is important to notice that the domain of clocks is the non-negative reals, thus the state space of a timed automaton is infinite. The edges of the timed automaton are annotated with guards and updates. Guards are conditions over the clocks; the edge is enabled if and only if the guard is satisfied. Updates are assignments that set the clock to a new value whenever the edge is taken. Finally, the vertices (which are called locations in timed automata) are labelled with invariants. Invariants are conditions that must be satisfied whenever the automaton is in that location (it is important to notice that invariants are not a way of checking whether the conditions are satisfied; invariants are satisfied by definition of a timed automaton -- states where the invariant does not hold do not exist). The language used by UPPAAL is somewhat more powerful: It supports integer variables, records, constants, arrays, parallel composition of several timed automata (which might synchronize via channels), arithmetic expressions and even functions with loops and conditional statements. If you are new to timed automata and UPPAAL, we recommend reading the UPPAAL tutorial.

An LPTA is a timed automaton that is extended with one addition variable: The cost. This is a monotonically increasing variable over the non-negative reals. Initially, it is zero. It might be incremented on the edges as part of the update (impulse cost). It can also increment with the passage of time with a specified rate. E.g. if the rate is 3 and 2.3 time units pass, then the cost is incremented with 6.9. The cost cannot be tested upon in any guard or invariants, so it does not influence the behaviour of the system -- this is a very important restriction, as otherwise model checking of LPTA would become undecidable.

About AMETIST

Citing the AMETIST web-page:

The main objective of the AMETIST project was to develop a powerful modelling methodology supported by efficient computerized problem-solving tools for the modelling and analysis of complex, distributed real-time systems. In particular, the project addressed problems in connection with time-dependent behaviour and dynamic resource allocation. Problems of this type are manifested under different names in application domains such as manufacturing, transport, communication networks, real-time software and digital circuits. AMETIST intended to develop a unifying mathematical modelling framework for these phenomena based on the existing body of theory and tools for the so-called timed automata model, which has emerged as a very promising formalism for the modelling and analysis of real-time related phenomena. By doing so we moved the state-of-the-art to a new level of maturity.