# Specifying Autonomous System Behaviour
Formal Specifications and their Challenges

Andrew Sogokon1, Burak Yuksek2, Gokhan Inalhan2, Neeraj Suri1

( 1 School of Computing and Communications, Lancaster University, UK
2 School of Aerospace, Transport and Manufacturing, Cranfield University, UK

)

###### Abstract

Specifying the intended behaviour of autonomous systems is becoming
increasingly important but is fraught with many challenges. This technical
report provides an overview of existing work on specifications of autonomous
systems and places a particular emphasis on _formal specification_ , i.e.
mathematically rigorous approaches to specification that require an
appropriate formalism. Given the breadth of this domain, our coverage is
necessarily incomplete but serves to provide a brief introduction to some of
the difficulties that specifying autonomous systems entails, as well as
existing approaches to addressing these difficulties currently pursued in
academia and industry.

##  1 Introduction

Autonomous systems are commonly understood to be systems that are capable of
decision making independently of their operator; these can be purely discrete
computer systems (e.g. software artefacts) or cyber-physical systems (CPS)
which operate in a physical environment (e.g autonomous vehicles). Modern
autonomous systems in the CPS domain may employ machine learning components in
their control loop and there is a degree of ambiguity about what precisely
constitutes a genuine _specification_ for an autonomous system (here by a
_specification_ we shall understand a description of what a system should do).
In applications where the autonomous system is designed to perform a function
that is also commonly performed by human operator, it has previously been
suggested (e.g. in [FDW13], [WFCJ11]) that the specification of autonomous
system behaviour (or the component responsible for autonomy in a given system)
is fundamentally linked to the certification of the human who could otherwise
operate the system if it were non-autonomous. In safety-critical applications
where malfunction can lead to disastrous outcomes (such as loss of life) it
becomes important to specify the desired behaviour precisely and
unambiguously, which can be highly non-trivial. Formal logics (e.g. see
[FDW13]) can be employed to precisely describe the desired system behaviour
(such as e.g. the requirement that collisions with obstacles must be avoided
throughout the duration of the system’s operation) and can provide a certain
standard for rigorous specifications.

######  Remark 1.

There exist a large number of formalisms for both modelling system behaviour
and specifying the desired system properties (a helpful review may be found in
the recent survey by Luckcuck et al. [LFD+19]); these formalisms vary in what
properties may be expressed and what systems may be modelled. For example,
_temporal properties_ such as a system attaining a certain state in the future
or a system never colliding with obstacles are examples of properties which
can be stated (i.e. formally specified) using _temporal logic_ (which we
briefly describe in latter sections); however, if one indeed intends to treat
an autonomous system _as a human_ , one may also wish to reason about the
_beliefs_ of this system in order to judge whether its actions are justified.
The choice of logic in which one wishes to formally express the specification
is thus highly significant.

While formal specifications are standard in areas of computer science that
align closely with _formal methods_ , they are presently not very widespread
within industrial practice, where carefully worded natural language prose is
still commonly employed to specify the intended behaviour of artefacts. The
challenges of formalising natural language requirements have long been
recognised [MK20], not least because practitioners find logical formalism
counter-intuitive (see e.g. [Hol19]). The most prominent applications of
formal system modelling and specification have to date been largely confined
to the design of _safety-critical systems_ where the cost of malfunction is
deemed prohibitive. The natural language requirements for such a system are
typically elaborated in a _requirements document_ and a formal model can be
developed with respect to a formalisation of these requirements (see e.g.
[Hoa13]). The use of formal methods in industrial projects, while uncommon,
has seen some notable successes, such as the design of a driverless airport
shuttle system [Abr06]. 111Notwithstanding these successes, it has been
remarked that one of the main problems in applying formal methods such as the
B method is the fact that the requirements document is often either badly
written or altogether missing [Abr07].

The following sections will review some of the existing work and identify
challenges in specifying the behaviour of autonomous systems, in particular
with regard to imprecise regulations, which autonomous systems are expected to
comply with.

##  2 Specifications Stemming from Regulation

As human operators are typically subject to regulations that outline
acceptable behaviour (e.g. the _Highway Code_ for road safety and vehicle
rules, or the _Rules of the Air_ for piloted aircraft), the regulations
themselves provide an immediate source of specifications for autonomous
systems in which the human operator is dispensed with. Unsurprisingly,
existing regulations were designed and written to be interpreted by humans and
are therefore stated in natural language. While in theory one may take
existing regulation such as the Highway Code/Rules of the Air and replace the
word ‘driver’/‘pilot’ with ‘autonomous system’, the resulting natural language
document will remain imprecise and will constitute an ambiguous set of
specifications.

###  2.1 Terrestrial Domain

In the terrestrial domain, e.g. when dealing with autonomous cars, a typical
mission simply involves navigating the vehicle from its current position to
the desired geographic location; however, the main challenge lies in modelling
and validating acceptable road behaviour along the way (as well as reasoning
about expected and unexpected behaviour of human drivers) [KGEH+21].

As in the aerial domain, regulations (traffic laws) exist in the terrestrial
domain and provide the bulk of the specifications for the intended behaviour
of autonomous cars. While these laws can, in some cases, be well defined and
lead to some anticipated safety requirements such as ensuring collision
freedom, there is considerable ambiguity as to the interpretation of
“reasonable care” that drivers are required to exercise in order not to harm
other drivers. As remarked in [SSSS17], any interpretation of this
requirements must follow societal norms, _which may be subject to change_.

######  Remark 2.

When certifying human drivers, the driving instructor in a driving test
provides his/her _interpretation_ of the rules in the Highway Code and acts as
a monitor for violations with respect to this interpretation.

Shalev-Shwartz et al. at _Mobileye_ [SSSS17] attempted to meet this challenge
by providing their own unambiguous interpretation of “reasonable care” and
proposed _responsibility-sensitive safety_ (RSS), which is summarised in five
“common sense” rules:

  * •

Do not hit someone from behind.

  * •

Do not cut-in recklessly.

  * •

Right-of-way is given, not taken.

  * •

Be careful of areas with limited visibility.

  * •

If you can avoid an accident without causing another one, you must do it.

In order to give an unambiguous interpretation of these rules, a formalisation
is undertaken in [SSSS17] which does not employ temporal logic like Fisher’s
work [FDW13], but takes a more conventional approach in making notions such as
e.g. the minimum safe distance between vehicles mathematically precise by
phrasing these requirements explicitly in reference to a mathematical model in
first-order logic.

######  Remark 3.

The RSS rules in [SSSS17] have been critiqued for their focus on ensuring that
the autonomous vehicle does not cause an accident [TGAF20] (i.e. cannot be
blamed for causing one), rather than avoiding accidents altogether.

Figure 1: Interpreting “duty of care”/“endangering” other vehicles

A rather different formalisation effort which also focused on traffic rules
for autonomous vehicles is described in the work of Rizaldi et al [RKH+17],
who formalised some (German) traffic rules that govern overtaking vehicles,
such as “ _when changing the lane to the left lane during overtaking, no
following road user shall be endangered._ ”. In this work, once again, the
authors needed to provide a precise meaning of ‘endangered’ in the informal
regulations document (a process which the authors termed “concretisation”).
The work in [RKH+17] is noteworthy for employing a theorem proving system
(Isabelle) to formalise a subset of traffic rules.

Regulations in the terrestrial domain concern more than just road vehicles.
For example, all new railway tracks and rolling stock on European railways are
legally reqired to adopt the European Train Control System (ETCS). The
specification of ETCS describes how trains move and periodically receive a
Movement Authority. Natural language requirements such as “ _The train trip
shall issue an emergency brake command, which shall not be revoked until the
train has reached standstill and the driver has acknowledged the trip_ ”. A
formalisation of requirements such as these was undertaken by Cimatti et al.
in [CRT09]. Platzer’s later work [PQ09] on ETCS formalisation and verification
employed a different formalism and a special purpose theorem proving system
(KeYmaera [PQ08]). This system was also employed by Loos et al. [LPN11] to
formally verify safe separation between road vehicles.

######  Remark 4.

The environment in which autonomous vehicles operate provides a big source of
uncertainty when it is not controlled, which in turn makes it difficult to
guarantee properties resulting from the interaction of the vehicle with the
environment. This fact has long been appreciated, along with the fact that the
environment is in practice very difficult to model, which leads one to having
to consider abstractions. One common way to address this issue is described by
Fremont, Sangiovanni-Vincentelli and Seshia [FSVS21] who argue that in order
to specify the behaviour of autonomous vehicles one needs to state assumptions
about the environment as part of a _contract_.

####  2.1.1 Notions of Safety

An important distinction exists between so-called _functional safety_ and
_nominal safety_ [SSSS17], where functional safety is concerned with hardware
and software failures that can lead to a safety hazard (as covered in ISO
26262) and nominal safety concerns itself with the safety of the logical
decisions of an autonomous vehicle, assuming that there are no hardware or
software malfunctions.

Absence of collisions with cars and other obstacles, which is the most common
form of specification that has been addressed in existing literature, along
with similar requirements such as ensuring safe separation between vehicles
[LPN11] would fall under the definition of nominal safety.

On the other hand, many industrial requirements fall under the definition of
functional safety. Some interesting examples can be found in the recently
proposed benchmarks contributed by Eddeland et al. [EDMÅ20], which feature
(modified) safety specifications from the Volvo Car Corporation. Safety
requirements in this instance are those properties that must hold at all
times.222The specifications are available on GitHub
https://github.com/decyphir/ARCH20_ATwSS/tree/master/STLFiles

###  2.2 Aerial Domain

A notable investigation into the use of formal specification and verification
(using an automated verification technology known as  _model checking_) in
order to prove that a control system of an autonomous aircraft follows _Rules
of the Air_ was reported by Webster et al. in [WFCJ11]. As remarked above,
this part of the specification for the autonomous system is in effect provided
by the _Civil Aviation Authority_ in the form of a natural language
regulations document which describes what behaviour is expected from a pilot.
The overall goal of this work was to establish some form of “human
equivalence” of the UAV with respect to the existing regulations. In order to
(partly) achieve this, the authors followed a scheme illustrated in Fig. 2,
where a selection of important regulations is picked out, formalised (i.e.
stated unambiguously in a formal logic) and evaluated against a _model_ of the
UAV, which provides a mathematical abstraction which can be analysed with
respect to the formal specification.

######  Remark 5.

The scheme in Fig.2 follows a familiar pattern used in formal modelling and
verification where the real world model is abstracted to an appropriate
abstract model and the informal requirements are mapped to a formal
specification (the interested reader may find a good overview in J. Wing’s
article. [Win90]).

The difficulty in specifying the behaviour of autonomous systems such as UAVs
subject to Rules of the Air precisely (formally) stems from the fact that
certain natural language passages are subject to multiple interpretations. The
document describing the Rules of the Air Regulations comprises some 15,000
words of natural language text. Formalising the rules in their entirety would
not be practically feasible. The work by Webster et al. instead focused on
formalising a very small subset of this document, namely the passages below

  * •

_“when two aircraft are approaching head-on and there is danger of collision,
each shall alter its course to the right”_ (sense and avoid),

  * •

“ _an aircraft in the vicinity of an aerodrome must make all turns to the left
unless told otherwise_ ” (navigation in airspace), and

  * •

“ _an aircraft shall not taxi on the apron or the manoeuvering area of an
aerodrome without permission_ ” (ATC clearance).

The formalisation of these statements was performed using temporal logic and
an automatic verification tool known as a _model checker_ was employed for
verification against a formal model. Naturally, this approach relies
critically on (i) the formalisation being correct (i.e. the semantics of the
formal specification being consistent with the intended meaning of the natural
language expressions) and (ii) on the quality of the model as a genuine
abstraction of the real system; if the model does not faithfully represent the
actual UAV, no meaningful equivalence can been established.

Rules of the AirUAVModelFormal specificationHuman equivalence?(Formal)
VerificationAbstractionSelection Figure 2: Certification approach pursued by
Webster et al. [WFCJ11]

It can, in practice, be difficult or impossible to formalise some other
requirements emanating from regulatory bodies that make reference to human
operators (such as pilots) of a certain level of skill being able to perform
certain functions. Specifications of this kind are not presently amenable to
formalisation.

The requirements considered in the work of Webster et al. are quite specific,
but the sense and avoid requirement is standard for aerial vehicles; though
its precise phrasing can vary (e.g “ _vigilance shall be maintained by each
person operating an aircraft so as to see and avoid other aircraft_ ” in
[FAA22]), the safety specification it is designed to ensure is that of
collision freedom and can be readily formalised.

The collision avoidance requirement is much more safety-critical in manned
aircraft than UAVs, which has motivated work on formal verification of
collision avoidance for systems equipped with ACAS (Airborne Collision
Avoidance System) X system by J-B Jeannin and co-authors in [JGK+15].

######  Remark 6.

Safety standards in aviation are often stated in probabilistic terms, e.g. “
_The acceptable level of risk (ALR) for UAS should be consistent across all
types of operations being performed, and no more restrictive than the accepted
fatality rates of general aviation_ ” [FAA22, AG 2.1], where fatality rates
are measured as the number of deaths per 100,000 flight hours.

Also, it needs to be stressed that the operating environment of both manned
aircraft and UAVs affects both the air and ground risks [FAA22]; for example,
a falling UAV may cause damage as it impacts the ground in a populated area.
Mitigating ground risks remains a _safety_ requirement, which at an abstract
level essentially amounts to the property of collision avoidance between
entities.

###  2.3 Safety Specifications

Formal requirements often combine _liveness_ (in computer science parlance a
property that “something good eventually happens”, such as a system attaining
a desirable state) and _safety_ , which in computer science is informally
understood as a property that “nothing bad happens” throughout the operation
of the system (e.g. the system never transitions into an undesirable state). A
typical example would be a specification for an autonomous vehicle which is
required to move from position $A$ to position $B$ in its environment, while
avoiding any obstacles along the way. Likewise, a swarm of UAVs may be
required to travel to a different location while avoiding collisions among the
UAVs along the way. These common kinds of requirements are sometimes termed
_reach-avoid_ and may be stated formally with reference to a particular
mathematical model.

Figure 3: Satisfying a reach-avoid requirement in an aerial setting

It needs to be stressed that in industrial practice _safety specifications_ do
not always align with the notion of safety used in computer science.
Specifications of safety-critical mission requirements are not limited to
properties such as avoiding obstacles or maintaining velocity (or temperature,
pressure, etc.) within prescribed operating bounds (i.e. the standard, but
narrow view of safety, as this term is employed in computer science). Safety-
critical requirements can in fact include many kinds of temporal properties,
such as:

  1. 1.

_eventuality_ – i.e. a form of liveness requiring that a _target_ set of
states is eventually attained by the system,

  2. 2.

_stability_ (of various kinds),

  3. 3.

operating within strict _deadlines_ ,

  4. 4.

_absence of oscillations_.

One may find an example of the latter safety-critical requirement for
_avoiding stick-slip oscillations_ in a model of a conventional oil well drill
string (described in more detail in [SJJ19]). Intuitively, the safety
specification for this system could be informally stated as: “ _the drill
pipes should not become damaged by the drilling bit repeatedly becoming stuck
and unstuck during the drill’s operation_ ”.

Specifications of system behaviour can be made precise using formal logics.
Temporal logics in particular have proved very useful as they permit one to
express many interesting properties that relate the states of the system to
time. Established temporal logics such as Linear Temporal Logic (LTL) were
first introduced to specify (and verify) the behaviour of computer programs,
but have since come to be used in fields such as robotics to specify motion
plans (a good overview of this application of LTL may be found in the article
by Plaku and Karaman [PK16]). Logics like LTL can express properties of
systems in which both state and time are discrete; as such, they can only be
applied to verify discrete abstractions of physical systems.

ABCDEF Figure 4: Visiting locations in an environment

For example, consider an environment illustrated in Fig 4 which can represent
an abstraction of a floor of a building where the regions near windows are
represented by cells coloured in blue and the cell coloured in green
represents the region containing a robot which can move in the plane by
transitioning into any neighbouring cell in a single time step. The language
of linear temporal logic provides _temporal operators_ (typically these are
$\Box$ : “always”; $\Diamond$ : “eventually”; $\mathcal{U}$ : “until”, and $X$
: “next”, i.e. “in the next state”) which allow us to formally express (i.e.
specify) properties of the desired motion of the robot. For example, the LTL
formula $\Diamond\phi$ expresses the property of eventuality of $\phi$, i.e.
the fact that _eventually_ the system enters a state where formula $\phi$ is
true. With this, one can formalise a simple surveillance task in which the
robot is required to visit all the regions near the windows on the floor as:

$\displaystyle\Diamond\,\mathsf{robAtB}\land\Diamond\,\mathsf{robAtC}\land\Diamond\,\mathsf{robAtD}\land\Diamond\,\mathsf{robAtE}\land\Diamond\,\mathsf{robAtF}\,,$

where $\mathsf{robAtB}$ represents the proposition “the robot is at location
B”, respectively for locations C, D, E and F.

######  Remark 7.

A very common kind of specification follows what is known as a _response
pattern_ , which specifies that it is always the case that an event P is
eventually followed by event Q, which takes the form

$\Box\left(P\to\Diamond Q\right)\,.$

While Linear Temporal Logic can be used to formally express many important
requirements that arise in practice, it does have limitations. For instance,
it is not possible to express the requirement that “ _it is always possible
for the robot to reach $D$_” (using the example in Fig. 6) in LTL. Instead,
such a requirement can be formally stated using Computational Tree Logic
(CTL), which likewise has been applied for specifying autonomous systems
[STWŻ11] and features so-called _path quantifiers_ $A$ (which may be
informally read as “along all computation paths”) and $E$ (“along at least one
computation path”) that are paired with path-specific quantifiers $G$
(“globally along the path”) and $F$ (“eventually along the path”). The above
requirement (which corresponds to a so-called _reset property_) can be
formalised in CTL as $\mathrm{AG}\,\mathrm{EF}\leavevmode\nobreak\
\mathsf{robAtD}$. Like LTL, CTL can also be used to express response pattern
in Rem. 7 as $\mathrm{AG}(P\to\mathrm{AF}\,Q)$; however, the property
expressed by the LTL formula $\Diamond\,\Box\,\mathsf{robAtD}$ cannot be
expressed in CTL. A logic that known as CTL∗ serves to combine the expressive
power of LTL and CTL.

The interested reader may find an accessible introduction to the temporal
logics LTL, CTL and CTL∗ in the excellent book by Huth and Ryan [HR04]. The
merits and important differences between the logics LTL and CTL, along with
their practical implications are also helpfully described by Vardi in [Var01].

In many practical applications (such as in real time systems and cyber-
physical systems), specifications involve _real_ time which does not advance
in discrete steps, as well as other continuously evolving variables. This
motivated the development of logics such as _Metric Temporal Logic_ (MTL)
[Koy90] and _Signal Temporal Logic_ (STL) [MN04], among others, in which the
temporal operators feature time constraints. For instance, a specification of
a collision avoidance property between a vehicle and an obstacle expressing
that the vehicle must maintain some minimum safe distance $d_{\min}>0$ from
the obstacle at all times in the future can be written down formally as:

$\Box_{[0,\infty)}\leavevmode\nobreak\ \mathsf{dist}(vehicle,obstacle)\geq
d_{\min}\,,$

where the temporal operator $\Box_{[0,\infty)}$ in the above formula expresses
_necessity_ and the formula may be read as “at all times in the future
$\mathsf{dist}(vehicle,obstacle)\geq d_{\min}$ holds”. The temporal operator
$\Diamond$, which expresses _eventuality_ , can feature a finite timing
constraint allowing us to write

$\Diamond_{[0,T]}\leavevmode\nobreak\ \mathsf{Target}\,,$

which informally says that the set of states described by the formula
$\mathsf{Target}$ is “eventually attained within $T$ time units”. A reach-
avoid specification can be expressed using a conjunction, i.e.

$\left(\Diamond_{[0,T]}\leavevmode\nobreak\
\mathsf{Target}\right)\leavevmode\nobreak\ \land\leavevmode\nobreak\
\left(\Box_{[0,T]}\leavevmode\nobreak\ \mathsf{Safe}\right)\,,$

where Safe is a formula describing the set of safe states of the system.

######  Remark 8.

We should note that the common _reach-avoid_ specifications can be stated in
purely set theoretic terms, i.e. by explicitly providing a set _Reach_ of
states that the system must enter (i.e. states satisfying Target) and a set
_Avoid_ of states that the system must avoid on its way to a state inside
_Reach_ (i.e. states satisfying Safe).

Properties such as absence of stick-slip oscillations in an oil drill
correspond to a temporal property known as _persistence_ (illustrated in Fig.
5(b)), which can be expressed using a nested combination of temporal
operators:

$\Diamond_{[0,T]}\leavevmode\nobreak\ \Box_{[0,\infty)}\leavevmode\nobreak\
\mathsf{Steady}\,,$

informally read as “ _eventually, within $T$ time units, the system enters the
$\mathsf{Steady}$ region and remains within it_”, where the formula Steady
represents bounds on the angular velocity with the lower bound being a
positive so as to ensure the angular velocity does not drop to zero which
could cause stick-slip oscillations (as in Fig. 5(a)).

$t$$0$angular velocity (a) Stick-slip oscillation

$t$$0$$|$$T$angular velocity (b) Persistence

Figure 5: Absence of stick-slip oscillations

Temporal logics such as LTL and STL have been applied in robotics to specify
and solve problems in motion control [CTB12], as well as multi-agent motion
planning [SCMF22]. Other formal logics, such as ATL (Alternating-time Temporal
Logic) [AHK02], permit one to formalise specifications that make reference to
cooperation among entities, such as e.g. “agents 1 and 2 can cooperate to
ensure that the system never enters a fail state” [vdHW12].

Differential dynamic logic (dL) was first introduced by Platzer [Pla08] and
provides a unified specification and verification framework for hybrid
systems. In this framework, a safety specification can take the form

$\mathrm{Init}\to[\alpha]\leavevmode\nobreak\ \mathrm{Safe}\,,$

where $\mathrm{Init}$ is a formula representing the set of initial states,
$\mathrm{Safe}$ is a formula representing the set of safe states of the
system, and $\alpha$ is a _hybrid program_ which provides an operational model
of the system itself; in this formula, the modal operator
$[\alpha]\leavevmode\nobreak\ \mathrm{Safe}$ means that the formula
$\mathrm{Safe}$ holds after all executions of hybrid program $\alpha$.
Differential _temporal_ dynamic logics have also been developed [Pla10, JP14],
which extend dL with temporal modalities $\Box$ and $\Diamond$.

######  Remark 9.

Having an operational model of the system be part of the formula that provides
the specification in dynamic logic is rather different to the situation with
temporal logics such as LTL, where one typically has a finite state model of
the system $S$, separately an LTL property $P$ which provides the
specification, and wishes to check whether the system satisfies the
specification (often written $S\models P$).

As a modelling formalism, hybrid programs provide constructs for assigning
values to variables, creating loops, conditionals, as well as letting
variables evolve continuously according to _differential equations_. Hybrid
programs thus provide an alternative to _hybrid automata_ [Hen00], which is
another popular model for cyber-physical systems.

Differential dynamic logic has been used in numerous works to specify (and
formally verify) the behaviour of terrestrial vehicles [MGP13, BTM+19];
Selvaraj et al. recently applied this formal framework to safe autonomous
driving [SAF22] and describe some important nuances in formal modelling
[SKAF22].

It is interesting to note that Signal Temporal Logic was originally introduced
for _monitoring_ properties of signals, rather than for verification of these
properties; it has proved convenient and has seen some use in industry. In
contrast, differential dynamic logic dL was from the outset designed to
support a calculus for constructing formal proofs. Recent work by Ahmad and
Jeannin [AJ21] introduced a Signal Temporal Dynamic Logic (STdL) which
attempts to bridge these differences.

###  2.4 Hyperproperties

Not all specifications can be directly stated as properties using temporal
logics such as LTL or STL. The notion of _hyperproperties_ was first
introduced by Clarkson and Schneider [CS10] in their study of security
properties and intuitively requires more than one trace (i.e. execution of the
system) in order to check, in contrast to standard trace properties that one
can express in logics like LTL.

######  Remark 10.

In formal methods, the notion of a _property_ is usually identified with a
_set of traces_ (a subset of all possible traces $Tr$). Thus, to say that a
system $S$ satisfies property $P$ (i.e. $S\models P$) simply means $S\subseteq
P$. The computer science notion of safety is an example of such a trace
property. In contrast, _hyperproperties_ are subsets of the powerset $2^{Tr}$.

$s_{6}$$s_{57}$ Figure 6: Taking an optimally short path as part of the
specification

To appreciate the difference between hyperproperties and trace properties it
is helpful to consider an example. Suppose we have a system which provides an
abstraction of a terrestrial robot navigating an environment illustrated in
Fig. 6, where rectangular cells represent the regions where the robot can be
situated and correspond discrete states of the system. The system is
initialised in state $s_{6}$ (i.e. the robot starts operating from the region
in the green cell in Fig. 6) and is required to transition to state $s_{57}$
(i.e. the region represented by the red cell) _in the fewest possible number
of steps_ without entering any of the forbidden regions coloured in black; the
system may transition into any of its neighbouring states (cells) in a single
step. In this example, it is possible to determine from a single trace
(execution, i.e. a sequence of states such as $s_{6}s_{5}s_{4}s_{12}\dots$) of
the system whether the required state $s_{57}$ is attained at some point, but
it is impossible to judge whether this trace is optimally short; in order to
do this, one requires access to all the other traces of the system which
attain $s_{57}$ in order to compare them. Optimality therefore provides an
example of a hyperproperty. This and other applications of hyperproperties in
robotics, in particular in robot motion planning are described in the recent
work by Wang et al. [WNP20].

Hyperproperties are of interest in security because they enable one to specify
e.g. the susceptibility of a system to side channel attacks [NKJ+17]. Logics
for hyperproperties have been developed by Clarkson et al. [CFK+14]. In cyber-
physical systems Nguyen et al. [NKJ+17] explored the use of hyperproperties
for specifying security and stability requirements and proposed a new formal
logic HyperSTL, which extends STL.

###  2.5 Issues with Temporal Logic Formalisations and Tool Support

It has been appreciated for some time that – even when there is no ambiguity –
fairly innocent informal specifications of system behaviour can require rather
unwieldy temporal logic formulas. Dwyer et al. [DAC99] give the following
example of a lift behaviour specification: “ _Between the time an elevator is
called at a floor and the time it opens its doors at that floor, the elevator
can arrive at that floor at most twice_.” Infamously, formalising this
specification in LTL (using the “until” temporal operator $\mathcal{U}$, in
addition to $\Box$ and $\Diamond$) one arrives at:

$\displaystyle\square\leavevmode\nobreak\ ((call\land\lozenge open)\to$
$\displaystyle\quad\quad((\lnot atfloor\land\lnot open)\leavevmode\nobreak\
\mathcal{U}$ $\displaystyle\quad\quad\quad(open\lor((atfloor\land\lnot
open)\leavevmode\nobreak\ \mathcal{U}$
$\displaystyle\quad\quad\quad\quad(open\lor((\lnot atfloor\land\lnot
open)\leavevmode\nobreak\ \mathcal{U}$
$\displaystyle\quad\quad\quad\quad\quad(open\lor((atfloor\land\lnot
open)\leavevmode\nobreak\ \mathcal{U}$
$\displaystyle\quad\quad\quad\quad\quad\quad(open\lor(\lnot
atfloor\leavevmode\nobreak\ \mathcal{U}\leavevmode\nobreak\ open)))))))))\,.$

The work of Dwyer et al. in [DAC99] sought to develop a _specification pattern
system_ to organise commonly occurring specification _patterns_ into a
hierarchy so as to facilitate formalisation of common high-level requirements.

Tools such as _FRET_ (Formal Requirements Elicitation Tool) [GMR+20] have been
developed at NASA to help with the formalisation of requirements. The idea
behind this approach is to adopt a restricted natural language with precise
semantics in which users can write informal requirements which can then be
formalised in temporal logic. More recently, He et al. [HBN+22] developed a
tool DeepSTL which is designed to translate informal English language
requirements into Signal Temporal Logic specifications.

##  3 Mission Specifications

As remarked in Sec. 2, regulations provide a large corpus of _de facto_
specifications for autonomous systems; these can be thought of as constraints
on their desired behaviour. If it is possible to respect these constraints,
the main task lies in specifying the _mission_ of an autonomous system.
Mission specifications are generally not restricted to autonomous systems (but
certain missions may e.g. be deemed too dangerous for a human operator to be
involved, or take place in an inhospitable environment which may require full
autonomy) and span a very wide spectrum of applications. Below we list some
existing work on formal specification of missions.

##### Catalogues of robotic missions

Menghi et al. created a catalogue of mission specifications that are commonly
employed in robotics [MTP+19] and provide temporal logic _templates_ for these
missions (the templates are available online
https://dsg.tuwien.ac.at/team/ctsigkanos/patterns/). For example, the intent
of _fair patrolling_ mission is defined by the authors in natural language as
“ _This pattern requires a robot to keep visiting a set of locations in a fair
way, i.e., the robots patrols the locations by keeping the number of times
every area is patrolled equal._ ”, which is subsequently formalised in LTL and
CTL. Recent work by Mallozzi et al. on contract-based robotic mission
specification [MNPS20] likewise employed Linear Temporal Logic in formalising
the requirements.

##### Surveillance

The work by Smith et al. [STBR11] considered path planning for surveillance
missions and employed Linear Temporal Logic (LTL). An example mission for a
robot in a (given) model of a terrestrial environment is [STBR11]:
_“Repeatedly gather data at locations g1, g2, and g3. Upload data at either u1
or u2 after each data-gather. Follow the road rules, and avoid the road
connecting i4 to i2.”_ (where the road intersections in the environment are
labelled with $i$, the gathering locations are labelled with $g$ and the
upload locations are labelled with $u$). Such a mission can be formally
written down using LTL formulas (see [STBR11, §5]). Furthermore, the authors
sought to generate _optimal_ robot paths; however, optimality is not directly
expressed in the formal logic as part of the specification and is rather
ensured by the algorithm developed in this work.

##### Hitting targets

In [KF08], Karaman and Frazzoli consider the _Multiple-UAV Mission Planning
problem_ , in which one is given a set of targets and a set of UAVs and one is
required to assign the targets to UAVs in an optimal manner (as well as
generate the optimal paths that each UAV has to follow). A case study
featuring a mission specification inspired by a military scenario is described
in [KF08]: “ _The mission in this case is to destroy either T1 and T3, or T2
and T3. Thus making a way through for the infantry from T1 side or T2 side.
There is also another specification which is that if the rescued unit escapes
from T2 side and reaches the friendly base C2 then V4 must meet the rescued
unit there with necessary health supplies_ ” (here the UAVs are denoted by
$V$, the targets by $T$). The overall specification can be formalised as a
conjunction of LTL constraints (see [KF08, §V]). In this work, once again, the
LTL specification is viewed as a _constraint_ , subject to which an
optimisation problem can be encoded and solved, i.e. optimality itself is not
expressed within the logic formalism.

##### Station keeping

Martin et al. [MGGP17] consider _station keeping manoeuvres_ of a Dubins
vehicle. A station keeping manoeuvre requires that “ _the vehicle reaches a
neighbourhood of its station in finite time and remains in it while waiting
for further instructions._ ” Such a manoeuvre is a combination of a liveness
(eventuality) property (i.e. the vehicle must reach the neighbourhood of its
station in finite time) and a safety property (i.e. the vehicle is to remain
in the neighbourhood of its station once it is there). The combination of the
two requirements results in a _persistence_ property which can be stated and
verified in differential dynamic logic, as done in [MGGP17] (although this
property could also be stated using a logic such as STL).

###  3.1 Challenges for Verification

Formalisms like temporal logics often allow us to precisely write down (i.e.
specify) requirements for the behaviour of systems. The task of _verifying_
these requirements for a given formal model of a system can often be a far
more difficult task, which is generally _undecidable_ and thus cannot be
performed automatically for many interesting systems. Nevertheless,
verification of formal requirements is sometimes possible

  1. 1.

For purely discrete models of systems, formal specifications in temporal
logics such as LTL can be verified _automatically_ using model checking (e.g.
see [HR04]). As a purely automated verification technology, model checking has
proved tremendously successful and has been applied in large industrial
verification problems (particularly in hardware verification). A number of
mature model checking tools are available, such as NuSMV [CCG+02], nuXmv
[CCD+14] and SPIN [Hol97].

The challenge in applying model checking as a verification technology to
cyber-physical systems lies in the fact that one cannot _in practice_ compute
reachable sets of continuous systems exactly (even up to finite time bound)
and is forced to over-approximate. These and other difficulties are described
in the work of Fehnker and Krogh in [FK04].

  2. 2.

Verification of _bounded-time_ properties, such as safety for a bounded
duration of time, eventuality and reach-avoid properties is often possible by
employing one of a family of methods – broadly known as _reachability
analysis_. Bounded-time verification is closely related to a verification
approach known as _bounded model checking_ (BMC) [BCC+09]. Some of the more
successful recent verification tools for _continuous_ and _hybrid_ dynamical
systems based on reachability analysis are _SpaceEx_ by Frehse et al.
[FGD+11], which works for linear systems, and _Flow*_ by Chen et al. [CÁS13]
which can also handle non-linear dynamics.

  3. 3.

An alternative verification technology to model checking is known as _theorem
proving_. Verification of important properties such as maintaining a safe
distance from obstacles at all times can be achieved by creating a formal
proof of such a property inside a theorem prover (also known as an
_interactive proof assistant_). Safety properties are typically require
finding appropriate _invariants_ , which in itself can be a difficult task.

The theorem proving approach to verification is much less automatic than model
checking and typically requires a considerable level of expertise to be
productive. The amount of effort involved in constructing formal proofs has
historically hindered the use of theorem provers in industry. However, it
needs to be stressed that theorem provers provide an unrivalled level of
assurance because they can produce fully rigorous formal proofs (in contrast
to model checking tools).

Some noteworthy efforts in cyber-physical system verification using theorem
provers are those pursued in the KeYmaera X prover [FMQ+15] (developed at
Carnegie Mellon University in a group led by A. Platzer), and the Hybrid Hoare
Logic (HHL) prover [WZZ15] (developed at the Chinese Academy of Sciences by N.
Zhan, S. Wang, and others).

Lamport’s temporal logic of actions [Lam94] was originally developed for
reasoning about concurrent systems (but has also been applied to model and
reason about physical systems [Lam92]) and enjoys extensive tool support in
the form of the TLA+ Toolbox [KLR19]; this framework is notable for its
successful application in the computer industry (see e.g. [New14]).

##### Specifications for Neural Networks

The increasing prevalence of components such as neural networks in autonomous
system designs presents a huge challenge to formal verification, not least
because a specification for the behaviour of these components is typically
absent. Indeed, some of the main issues with the use of machine learning
components in autonomous systems stem from the difficulty of precisely
specifying their intended behaviour. This problem brought on by the _absence
of a specification for the components of a system_ (e.g. lack of specification
for a neural net component) even when a formal specification exists for the
overall system (e.g. given by a temporal logic formula) is discussed in the
work of Seshia and co-workers [SDD+18], who argue that the overall system
specification should serve as a starting point from which one can try to
_derive_ component specifications.

##  4 Control System Specifications

In autonomous systems, control algorithms are utilised to provide stability of
the whole system and meet the signal tracking requirements to perform
specified mission with minimum error. These requirements for the control
systems are directly related to operational safety and should be defined
clearly for an effective validation and verification process. For an advanced
air mobility (AAM) vehicle, schematics of a closed-loop system is given in
Figure 7. As shown in this figure, there are two fundamental loops that
consist of the flight control system; a) Inner-loop attitude control system,
and b) outer-loop trajectory tracking system. In the following sections, we
briefly review some control specifications for both the inner-loop and outer-
loop controllers.

Figure 7: Overview of the cascaded flight control system.

###  4.1 Attitude Control System Specifications

It is generally recognised that the use of rigorous analysis methods at the
beginning of requirement development phase of the control system design
process significantly reduces the software development costs. In [Gro17], an
approach is presented in which common spacecraft system requirements such as
actuator limits, steady state error, settling time, rise time and overshoot
are formalised. The proposed approach enables analysis of the requirements in
early stages of system development. Formalisation and analysis of aerospace
control requirements have been studied for decades but the focus has been on
the high level requirements and mode logic. In contrast, the focus in [Gro17]
is on providing a formal description for low-level control system
requirements.

Some hypothetical requirements for an attitude control system with four wheel
Reaction Wheel Array (RWA) are described in [GHC+15, Gro16, Gro17] which we
will briefly review below. The first two requirements for constraining the
outputs of a control system are designed to prevent damage to the spacecraft
and are given as follows:

  * •

R01: “The commanded time rate of change of angular velocity shall not exceed
the maximum allowable angular acceleration of the reaction wheel.”

  * •

R02: “The commanded angular velocity shall not exceed the maximum allowable
angular velocity of the reaction wheel”

Requirements such as these represent examples of safety specifications where
variables are required to never exceed certain given bounds; these bounds in
effect represent global invariants and properties such as these can be readily
formalised in logics such as STL and dL.

Other kinds of requirements considered by Gross in [Gro17] feature a safety
element while also specifying aspects of the expected _performance_ of the
attitude control system:

  * •

R03: “The pointing accuracy shall be less than 1 degree as a threshold and
0.08 degrees as an objective.”

  * •

R04: “The pointing range about the z axis shall be 0 to 360 degrees.”

  * •

R05: “The pointing range about the y axis shall be 0 to 360 degrees.”

  * •

R06: “The pointing range about the x axis shall be 0 to 360 degrees.”

  * •

R07: “The maximum slew rate shall be $>$ 3 deg/sec as a threshold and $>$ 7
deg/sec as an objective.”

  * •

R08: “After settling, the drift rate shall be $<$ 3 deg/min as a threshold and
$<$ 1 deg/min as an objective.”

  * •

R09: “After settling, the total drift shall be $\leq$ 0.5 degrees as a
threshold and $\leq$ 0.1 degrees as an objective.”

  * •

R10: “The 5% settling time shall be $\leq$ 5 minutes as a threshold and $\leq$
2 minutes as an objective.”

  * •

R11: “The 2% settling time shall be $\leq$ 7 minutes as a threshold and $\leq$
3 minutes as an objective.”

  * •

R12: “The rise time shall be $\leq$ 5 minutes as a threshold and $\leq$ 2
minutes as an objective.”

  * •

R13: “The percent overshoot shall be $\leq$ 50% as a threshold and $\leq$ 25%
as an objective.”

While ensuring that the thresholds (i.e. bounds) given in these requirements
are respected at all times is safety-critical, the “objective” part of these
requirements describe the desired performance characteristics, which are
highly desirable but not safety-critical. This presents a challenge: while it
is often possible to express the performance requirements formally, it is
important to distinguish between those that are safety-critical versus those
that are not.

An interesting potential solution to this issue involves creating a
_hierarchy_ of specifications, as described in the recent work of Berducci et
al. [BANG21], who treat a task specification as an _ordered set_ of safety,
target and comfort requirements, where the order reflects the level of
criticality. The fact that comfort (or performance) requirements may be
violated can be addressed using so-called _quantitative semantics_ of logics
such as STL (e.g. see [DFM13]). Quantitative semantics of STL has also been
recently employed by Chen et al. [CLSP22]) to formalise and reason about the
property of _resiliency_ in cyber-physical systems.

The practical use of formalisms such as temporal logic is as yet largely
unfamiliar outside of computer science and its use in domains such as
aerospace is presently very limited. Furthermore, instead of formal
verification, extensive _simulation_ /testing in commonly employed in the
certification process in practice. To give a sense of perspective on the
current state of specifications employed in practice, the following section
will briefly describe specifications based on so-called Mission-Task Elements.

###  4.2 Trajectory Tracking System Specifications: A Mission-Task Element
Approach

For rotary-wing aerial vehicles, flight test manoeuvres are provided as
_Mission-Task Elements_ (MTEs) in ADS-33E-PRF. The overall assessment of the
rotorcraft’s ability to perform certain tasks that constitute its mission,
such as hover, landing, acceleration-deceleration, is performed by utilising
MTEs and this process results in assigning a level of _Handling Qualities_
(HQ). A list of applicable MTEs for full-scale rotorcrafts is given in the
table below.

MTEs for Full-scale Rotorcrafts
---
Hover | Acceleration/Deceleration
Landing | Sidestep
Hovering Turn | Transient Turn
Pirouette | Pullup/Pushover
Depart/Abort | Turn to target
Lateral Reposition | Decelerating Approach
Slalom | Missed Approach

As a descriptive example for full-scale rotorcraft MTEs, we take a brief look
at the performance standards of hover flight below.

#### Performance Standards for Hover Flight Phase

  * •

Objectives: Checking the ability of transition from forward flight to hover
flight with precision and adequate aggressiveness level.

  * •

Performance Standards: Accomplishing the transition to hover flight while
meeting the performance requirements given in Figure 8.

Figure 8: Performance Specifications for Hover Flight.

#### Scaled-down MTEs for Autonomous Aerial Vehicles

Although the MTEs in ADS-33E-PRF are designed for piloted rotorcrafts, they
have also been utilised to evaluate the trajectory tracking capability of the
UAVs [YSC+20, IGW+18]. Here, kinematic scaling, which is a function of maximum
cruise velocity of the rotorcraft, is performed to scale-down the original
MTEs to obtain applicable missions for UAVs. Here, kinematic scaling is
applied to calculate spatial, velocity and time scale factors.

It is also required to define an _objective function_ to score the MTE
completion performance of the UAV. A weighted sum $(L)$ of the aggressiveness,
trajectory tracking performance, robustness is defined as given in Eq. (1) to
assess the manoeuvre. Then, $L$ is used to calculate the Trajectory Tracking
and Aggressiveness (TTA) score $\phi_{TTA}$ as given in Eq.(2). Here, $\alpha$
is aggressiveness level of the maneuver, $(\epsilon)$ is trajectory tracking
error, and $R$ is robustness. TTA score is between 0 and 100.

$L=w_{\alpha}\frac{\alpha-\alpha_{G}}{\alpha_{B}-\alpha_{G}}+w_{\epsilon}\frac{\epsilon-\epsilon_{G}}{\epsilon_{B}-\epsilon_{G}}+w_{R}\frac{R-R_{G}}{R_{B}-R_{G}}$
(1)

$\phi_{TTA}(L)=\frac{200}{1+e^{L}}$ (2)

The quantities $w_{a},w_{\epsilon},w_{R}$ are weights used to define the
relative importance of individual objectives. Subscripts ‘$B$’ and ‘$G$’ stand
for best and good possible values.

After calculating the TTA score by using above mentioned equations, the
overall system performance for specific manoeuvres is evaluated based on the
score tables given in Table 1 and 2 for nominal and aggressive flights,
respectively [IGW+18].

Table 1: Performance levels for nominal manoeuvring mission Maneuver |  | Desired TTA Score
---
(Level 1)
| Adequate TTA Score
---
(Level 2)
| Lateral Reposition
---
$\phi_{TTA}\geq 75$ | $75\geq\phi_{TTA}\geq 70$
Depart Abort | $\phi_{TTA}\geq 75$ | $75\geq\phi_{TTA}\geq 70$
Pirouette | $\phi_{TTA}\geq 73$ | $73\geq\phi_{TTA}\geq 68$
Table 2: Performance levels for aggressive maneuvering mission Maneuver |  | Desired TTA Score
---
(Level 1)
| Adequate TTA Score
---
(Level 2)
| Lateral Reposition
---
$\phi_{TTA}\geq 82$ | $82\geq\phi_{TTA}\geq 77$
Depart Abort | $\phi_{TTA}\geq 82$ | $82\geq\phi_{TTA}\geq 77$
Pirouette | $\phi_{TTA}\geq 80$ | $80\geq\phi_{TTA}\geq 75$

A descriptive example for scaled-down lateral reposition MTE is given in
Figure 9 [YSC+20]. In this test, a multirotor UAV is supposed to perform a
lateral reposition manoeuvre while following a triangular-shape velocity
profile. Velocity time histories for different agility levels are given in
Figure 10.

Figure 9: Lateral reposition flight test [YSC+20]. Figure 10: Velocity and
position time histories for scaled-down lateral reposition MTE [YSC+20].

Upon completing simulations and flight tests, TTA score analysis is performed
to evaluate the performance of the overall closed-loop system; the results are
presented in Figure 11. Here, both Monte Carlo studies in the simulation
environment and flight tests indicate that TTA scores for lateral reposition
and depart/abort maneuvers meet the Level-1 TTA requirements which are given
in Table 1 and 2.

Figure 11: TTA analysis results for different aggressiveness levels [YSC+20].

In summary, control system specifications for autonomous systems are highly
critical requirements which are directly connected with operation safety of
the vehicles. In operation environments such as urban areas, farms or even in
indoor environments, it is crucial to follow given reference signals (i.e.
reference trajectories for outer-loop and reference attitude for inner-loop)
to perform the given mission safely. If the vehicle could not track the given
signals properly, this might result in catastrophic accidents and affects the
system trust, directly. For these reasons, autonomous system specifications,
especially for aerial vehicles, should be investigated for two levels, a) low-
level attitude control loop, and b) trajectory tracking loop. Here, the former
one defines attitude command tracking requirements in time-domain such as
settling-time, rise-time and overshoot. An example is given which is applied
on attitude control system design process of a satellite system. A similar
approach could be applied for autonomous aerial and ground systems. The latter
one defines specifications based on aggressiveness level and signal tracking
error for trajectory tracking loop. A descriptive example is also given in
which flight tests are performed to evaluate the trajectory tracking
performance of a UAV. Here, it is shown that designed inner- and outer-loops
meet the trajectory tracking and aggressiveness requirements which are defined
by scaling-down the rotorcraft specifications. Results are validated in
simulation environment and flight tests. For future works, definitions of
autonomous system specifications could be defined for higher levels of the
loop such as mission planning algorithms which contain trajectory generation
and task assignment processes.

##  5 Conclusion

As autonomous systems become more widely adopted, the need for specifying
their behaviour will become ever more pressing. A lack of specification makes
it difficult or impossible to judge whether a system is functioning as
intended or if there are deficiencies in its design. Likewise, imprecise
specifications create difficulties from a regulatory standpoint; for instance,
if the system conforms to an _interpretation_ of a certain imprecise
requirement which is later found to be at variance with the interpretation by
the regulatory body. Rigorous specifications, on the other hand, should leave
no scope for ambiguity and hold the promise of enabling truly trustworthy
designs; the difficulties arise in the effort that is currently required to
describe the intended behaviour precisely and in the inherent complexity of
reasoning about this behaviour. At present, formal specifications for
autonomous systems cannot be said to be widely adopted by industry or
government regulatory bodies, but this state of affairs may change in future
if some of the difficulties inherent in formal specification and verification
surveyed in this article can be even partially overcome.

##### Acknowledgements:

The authors would like to thank Dr Cora-Lisa Perner at Airbus, Dr Wilfried
Steiner at TTTech Labs and Dr Oscar Gonzalez Villarreal at the School of
Aerospace, Transport and Manufacturing, Cranfield University for their
insights and interesting discussions. This work is supported by the UKRI
Engineering and Physical Sciences Research Council [EPSRC Grant number:
EP/V026763/1]

## References

  * [Abr06] Jean-Raymond Abrial.  Formal methods in industry: achievements, problems, future.  In Proceedings of the 28th International Conference on Software Engineering, pages 761–768, 2006.
  * [Abr07] Jean-Raymond Abrial.  Formal methods: Theory becoming practice.  J. Univers. Comput. Sci., 13(5):619–628, 2007.
  * [AHK02] Rajeev Alur, Thomas A Henzinger, and Orna Kupferman.  Alternating-time temporal logic.  Journal of the ACM (JACM), 49(5):672–713, 2002.
  * [AJ21] Hammad Ahmad and Jean-Baptiste Jeannin.  A program logic to verify signal temporal logic specifications of hybrid systems.  In Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control, pages 1–11, 2021.
  * [BANG21] Luigi Berducci, Edgar A Aguilar, Dejan Ničković, and Radu Grosu.  Hierarchical potential-based reward shaping from task specifications.  arXiv e-prints, pages arXiv–2110, 2021.
  * [BCC+09] Armin Biere, Alessandro Cimatti, Edmund M Clarke, Ofer Strichman, and Yunshan Zhu.  Bounded model checking.  Handbook of satisfiability, 185(99):457–481, 2009.
  * [BTM+19] Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Andrew Sogokon, and André Platzer.  A formal safety net for waypoint-following in ground robots.  IEEE Robotics and Automation Letters, 4(3):2910–2917, 2019.
  * [CÁS13] Xin Chen, Erika Ábrahám, and Sriram Sankaranarayanan.  Flow*: An analyzer for non-linear hybrid systems.  In International Conference on Computer Aided Verification, pages 258–263. Springer, 2013.
  * [CCD+14] Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta.  The nuxmv symbolic model checker.  In International Conference on Computer Aided Verification, pages 334–342. Springer, 2014.
  * [CCG+02] Alessandro Cimatti, Edmund Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella.  Nusmv 2: An opensource tool for symbolic model checking.  In International Conference on Computer Aided Verification, pages 359–364. Springer, 2002.
  * [CFK+14] Michael R Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K Micinski, Markus N Rabe, and César Sánchez.  Temporal logics for hyperproperties.  In International Conference on Principles of Security and Trust, pages 265–284. Springer, 2014.
  * [CLSP22] Hongkai Chen, Shan Lin, Scott A Smolka, and Nicola Paoletti.  An STL-based formulation of resilience in cyber-physical systems.  arXiv preprint arXiv:2205.03961, 2022.
  * [CRT09] Alessandro Cimatti, Marco Roveri, and Stefano Tonetta.  Requirements validation for hybrid systems.  In International Conference on Computer Aided Verification, pages 188–203. Springer, 2009.
  * [CS10] Michael R Clarkson and Fred B Schneider.  Hyperproperties.  Journal of Computer Security, 18(6):1157–1210, 2010.
  * [CTB12] Yushan Chen, Jana Tumova, and Calin Belta.  LTL robot motion control based on automata learning of environmental dynamics.  In 2012 IEEE International Conference on Robotics and Automation, pages 5177–5182. IEEE, 2012.
  * [DAC99] Matthew B Dwyer, George S Avrunin, and James C Corbett.  Patterns in property specifications for finite-state verification.  In Proceedings of the 21st International Conference on Software Engineering, pages 411–420, 1999.
  * [DFM13] Alexandre Donzé, Thomas Ferrere, and Oded Maler.  Efficient robust monitoring for STL.  In International Conference on Computer Aided Verification, pages 264–279. Springer, 2013.
  * [EDMÅ20] Johan Lidén Eddeland, Alexandre Donzé, Sajed Miremadi, and Knut Åkesson.  Industrial temporal logic specifications for falsification of cyber-physical systems.  EPiC Series in Computing, 74:267–274, 2020.
  * [FAA22] FAA.  Unmanned aircraft systems beyond visual line of sight aviation rulemaking committee, 2022.
  * [FDW13] Michael Fisher, Louise Dennis, and Matt Webster.  Verifying autonomous systems.  Communications of the ACM, 56(9):84–93, 2013.
  * [FGD+11] Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler.  SpaceEx: Scalable verification of hybrid systems.  In International Conference on Computer Aided Verification, pages 379–395. Springer, 2011.
  * [FK04] Ansgar Fehnker and Bruce H Krogh.  Hybrid system verification is not a sinecure.  In International Symposium on Automated Technology for Verification and Analysis, pages 263–277. Springer, 2004.
  * [FMQ+15] Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, and André Platzer.  KeYmaera X: an axiomatic tactical theorem prover for hybrid systems.  In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in Computer Science, pages 527–538. Springer, 2015.
  * [FSVS21] Daniel J Fremont, Alberto L Sangiovanni-Vincentelli, and Sanjit A Seshia.  Safety in autonomous driving: Can tools offer guarantees?  In 2021 58th ACM/IEEE Design Automation Conference (DAC), pages 1311–1314. IEEE, 2021.
  * [GHC+15] Kerianne Gross, Jonathan Hoffman, Matthew Clark, Eric Swenson, Richard Cobb, Michael Whalen, and Lucas Wagner.  Evaluation of formal methods tools applied to a 6u cubesat attitude control system.  In AIAA SPACE 2015 Conference and Exposition, page 4529, 2015.
  * [GMR+20] Dimitra Giannakopoulou, Anastasia Mavridou, Julian Rhein, Thomas Pressburger, Johann Schumann, and Nija Shi.  Formal requirements elicitation with FRET.  In International Working Conference on Requirements Engineering: Foundation for Software Quality (REFSQ-2020), number ARC-E-DAA-TN77785, 2020\.
  * [Gro16] Kerianne H Gross.  Evaluation of verification approaches applied to a nonlinear system control.  Technical Report AFIT-ENY-MS-16-M-214, Air Force Institute of Technology, Wright-Patterson Air Force Base, Ohio, 2016.
  * [Gro17] Kerianne H Gross.  Formal specification and analysis approaches for spacecraft attitude control requirements.  In 2017 IEEE Aerospace Conference, pages 1–11. IEEE, 2017.
  * [HBN+22] Jie He, Ezio Bartocci, Dejan Ničković, Haris Isakovic, and Radu Grosu.  Deepstl: From english requirements to signal temporal logic.  In Proceedings of the 44th International Conference on Software Engineering, ICSE ’22, page 610–622, New York, NY, USA, 2022. Association for Computing Machinery.
  * [Hen00] Thomas A Henzinger.  The theory of hybrid automata.  In Verification of Digital and Hybrid Systems, pages 265–292. Springer, 2000.
  * [Hoa13] Thai Son Hoang.  An introduction to the Event-B modelling method.  Industrial Deployment of System Engineering Methods, pages 211–236, 2013.
  * [Hol97] Gerard J. Holzmann.  The model checker SPIN.  IEEE Transactions on software engineering, 23(5):279–295, 1997\.
  * [Hol19] Gerard J Holzmann.  Formalizing requirements is $\lozenge\square$ hard.  In From Reactive Systems to Cyber-Physical Systems, pages 51–56. Springer, 2019.
  * [HR04] Michael Huth and Mark Ryan.  Logic in Computer Science: Modelling and Reasoning about Systems.  Cambridge University Press, 2004.
  * [IGW+18] C Ivler, C Goerzen, J Wagster, F Sanders, K Cheung, and M Tischler.  Control design for tracking of scaled mte trajectories on an iris+ quadcopter.  In AHS 74th Annual Forum, Phoenix, AZ, 2018.
  * [JGK+15] Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki, and André Platzer.  A formally verified hybrid system for the next-generation airborne collision avoidance system.  In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 21–36. Springer, 2015.
  * [JP14] Jean-Baptiste Jeannin and André Platzer.  dtl 2: differential temporal dynamic logic with nested temporalities for hybrid systems.  In International Joint Conference on Automated Reasoning, pages 292–306. Springer, 2014.
  * [KF08] Sertac Karaman and Emilio Frazzoli.  Complex mission optimization for multiple-uavs using linear temporal logic.  In 2008 American Control Conference, pages 2003–2009. IEEE, 2008\.
  * [KGEH+21] Hadas Kress-Gazit, Kerstin Eder, Guy Hoffman, Henny Admoni, Brenna Argall, Ruediger Ehlers, Christoffer Heckman, Nils Jansen, Ross Knepper, Jan Křetínskỳ, et al.  Formalizing and guaranteeing human-robot interaction.  Communications of the ACM, 64(9):78–84, 2021.
  * [KLR19] Markus Alexander Kuppe, Leslie Lamport, and Daniel Ricketts.  The TLA+ toolbox.  arXiv preprint arXiv:1912.10633, 2019.
  * [Koy90] Ron Koymans.  Specifying real-time properties with metric temporal logic.  Real-Time Systems, 2(4):255–299, 1990.
  * [Lam92] Leslie Lamport.  Hybrid systems in TLA+.  In Hybrid systems, pages 77–102. Springer, 1992.
  * [Lam94] Leslie Lamport.  The temporal logic of actions.  ACM Transactions on Programming Languages and Systems (TOPLAS), 16(3):872–923, 1994.
  * [LFD+19] Matt Luckcuck, Marie Farrell, Louise A. Dennis, Clare Dixon, and Michael Fisher.  Formal specification and verification of autonomous robotic systems: A survey.  ACM Comput. Surv., 52(5), sep 2019.
  * [LPN11] Sarah M Loos, André Platzer, and Ligia Nistor.  Adaptive cruise control: Hybrid, distributed, and now formally verified.  In International Symposium on Formal Methods, pages 42–56. Springer, 2011.
  * [MGGP17] Benjamin Martin, Khalil Ghorbal, Eric Goubault, and Sylvie Putot.  Formal verification of station keeping maneuvers for a planar autonomous hybrid system.  In FVAV 2017-1st Formal Verification of Autonomous Vehicles Workshop, volume 257, pages 91–104, 2017.
  * [MGP13] Stefan Mitsch, Khalil Ghorbal, and André Platzer.  On provably safe obstacle avoidance for autonomous robotic ground vehicles.  In Robotics: Science and Systems IX, Technische Universität Berlin, Berlin, Germany, June 24-June 28, 2013, 2013.
  * [MK20] Konstantinos Mokos and Panagiotis Katsaros.  A survey on the formalisation of system requirements and their validation.  Array, 7:100030, 2020.
  * [MN04] Oded Maler and Dejan Nickovic.  Monitoring temporal properties of continuous signals.  In Yassine Lakhnech and Sergio Yovine, editors, Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2004, Grenoble, France, September 22-24, 2004, Proceedings, volume 3253 of Lecture Notes in Computer Science, pages 152–166. Springer, 2004\.
  * [MNPS20] Piergiuseppe Mallozzi, Pierluigi Nuzzo, Patrizio Pelliccione, and Gerardo Schneider.  Crome: contract-based robotic mission specification.  In 2020 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), pages 1–11. IEEE, 2020.
  * [MTP+19] Claudio Menghi, Christos Tsigkanos, Patrizio Pelliccione, Carlo Ghezzi, and Thorsten Berger.  Specification patterns for robotic missions.  IEEE Transactions on Software Engineering, 47(10):2208–2224, 2019\.
  * [New14] Chris Newcombe.  Why amazon chose TLA+.  In International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, pages 25–39. Springer, 2014.
  * [NKJ+17] Luan Viet Nguyen, James Kapinski, Xiaoqing Jin, Jyotirmoy V Deshmukh, and Taylor T Johnson.  Hyperproperties of real-valued signals.  In Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, pages 104–113, 2017.
  * [PK16] Erion Plaku and Sertac Karaman.  Motion planning with temporal-logic specifications: Progress and challenges.  AI Communications, 29(1):151–162, 2016.
  * [Pla08] André Platzer.  Differential dynamic logic for hybrid systems.  Journal of Automated Reasoning, 41(2):143–189, 2008.
  * [Pla10] André Platzer.  Differential temporal dynamic logic dtl.  In Logical Analysis of Hybrid Systems, pages 203–230. Springer, 2010.
  * [PQ08] André Platzer and Jan-David Quesel.  Keymaera: A hybrid theorem prover for hybrid systems (system description).  In International Joint Conference on Automated Reasoning, pages 171–178. Springer, 2008.
  * [PQ09] André Platzer and Jan-David Quesel.  European train control system: A case study in formal verification.  In International Conference on Formal Engineering Methods, pages 246–265. Springer, 2009.
  * [RKH+17] Albert Rizaldi, Jonas Keinholz, Monika Huber, Jochen Feldle, Fabian Immler, Matthias Althoff, Eric Hilgendorf, and Tobias Nipkow.  Formalising and monitoring traffic rules for autonomous vehicles in isabelle/hol.  In International conference on integrated formal methods, pages 50–66. Springer, 2017.
  * [SAF22] Yuvaraj Selvaraj, Wolfgang Ahrendt, and Martin Fabian.  Formal development of safe automated driving using differential dynamic logic.  arXiv preprint arXiv:2204.06873, 2022.
  * [SCMF22] Dawei Sun, Jingkai Chen, Sayan Mitra, and Chuchu Fan.  Multi-agent motion planning from signal temporal logic specifications.  arXiv preprint arXiv:2201.05247, 2022.
  * [SDD+18] Sanjit A. Seshia, Ankush Desai, Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Sumukh Shivakumar, Marcell Vazquez-Chanlatte, and Xiangyu Yue.  Formal specification for deep neural networks.  In Shuvendu K. Lahiri and Chao Wang, editors, Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings, volume 11138 of Lecture Notes in Computer Science, pages 20–34. Springer, 2018\.
  * [SJJ19] Andrew Sogokon, Paul B. Jackson, and Taylor T. Johnson.  Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants.  J. Autom. Reasoning, 63(4):1005–1029, 2019.
  * [SKAF22] Yuvaraj Selvaraj, Jonas Krook, Wolfgang Ahrendt, and Martin Fabian.  On how to not prove faulty controllers safe in differential dynamic logic.  In International Conference on Formal Engineering Methods, pages 281–297. Springer, 2022.
  * [SSSS17] Shai Shalev-Shwartz, Shaked Shammah, and Amnon Shashua.  On a formal model of safe and scalable self-driving cars.  arXiv preprint arXiv:1708.06374, 2017.
  * [STBR11] Stephen L Smith, Jana Tumova, Calin Belta, and Daniela Rus.  Optimal path planning for surveillance with temporal-logic constraints.  The International Journal of Robotics Research, 30(14):1695–1708, 2011.
  * [STWŻ11] Gopinadh Sirigineedi, Antonios Tsourdos, Brian A White, and Rafał Żbikowski.  Kripke modelling and verification of temporal specifications of a multiple UAV system.  Annals of Mathematics and Artificial Intelligence, 63(1):31–52, 2011.
  * [TGAF20] Mario Henrique Cruz Torres, Jean-Pierre Giacalone, and Joelle Abou Faysal.  A case study on formally validating motion rules for autonomous cars.  In International Conference on Software Engineering and Formal Methods, pages 233–248. Springer, 2020.
  * [Var01] Moshe Y. Vardi.  Branching vs. linear time: Final showdown.  In TACAS 2001, volume 2031 of LNCS, pages 1–22. Springer, 2001.
  * [vdHW12] Wiebe van der Hoek and Michael Wooldridge.  Logics for multiagent systems.  AI Magazine, 33(3):92–92, 2012.
  * [WFCJ11] Matt Webster, Michael Fisher, Neil Cameron, and Mike Jump.  Formal methods for the certification of autonomous unmanned aircraft systems.  In International Conference on Computer Safety, Reliability, and Security, pages 228–242. Springer, 2011.
  * [Win90] Jeannette M Wing.  A specifier’s introduction to formal methods.  Computer, 23(9):8–22, 1990.
  * [WNP20] Yu Wang, Siddhartha Nalluri, and Miroslav Pajic.  Hyperproperties for robotics: Planning via hyperltl.  In 2020 IEEE International Conference on Robotics and Automation (ICRA), pages 8462–8468. IEEE, 2020.
  * [WZZ15] Shuling Wang, Naijun Zhan, and Liang Zou.  An improved HHL prover: An interactive theorem prover for hybrid systems.  In Michael J. Butler, Sylvain Conchon, and Fatiha Zaïdi, editors, Formal Methods and Software Engineering - 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings, volume 9407 of Lecture Notes in Computer Science, pages 382–399. Springer, 2015.
  * [YSC+20] Burak Yuksek, Emre Saldiran, Aykut Cetin, Ramazan Yeniceri, and Gokhan Inalhan.  System identification and model-based flight control system design for an agile maneuvering quadrotor platform.  In AIAA Scitech 2020 Forum, page 1835, 2020.