# 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.