|
Title
|
|
|
|
Learning and verifying temporal specifications for cyber-physical systems
| |
|
Author
|
|
|
|
| |
|
Abstract
|
|
|
|
| In the past decade, there has been an unprecedented rise in the incorporation of cyber-physical systems used to perform complex tasks. Verifying these systems is necessary to ensure their safety and reliability, especially in safety-critical scenarios. Formal verification has been proven to be a time-tested method to systematically verify these systems. In particular, it provides techniques for monitoring system executions against a formal specification. Temporal logic has gained popularity as a formal specification due to its mathematical rigour, human interpretability, and compatibility with various formal verification techniques. But, often, these specifications are hard to design manually, necessitating a need to automatically generate them from system executions. The objective of this thesis is twofold: (i) Develop algorithms to automatically learn temporal specifications from system executions; (ii) Apply formal verification techniques to assess the correctness of the system against the acquired specifications. To achieve these objectives, in the learning part, we present two algorithms to learn specifications in temporal logics such as LTL, MTL, and STL. We present a dynamic programming-based algorithm for LTL specifications that leverages a normal form for a fragment of LTL and uses efficient enumeration techniques to learn concise formulas from system executions. For MTL and STL, we develop SMT-solver-based techniques to learn formulas that are not only concise but also efficient to be applied for formal verification of the system. Our algorithms are implemented in tools called SCARLET and TEAL, and their efficiency is demonstrated through experimental results. In the verification part, we focus on the LTL parameter-synthesis problems of one-counter automata, one of the fundamental formal models to represent complex systems, namely systems with discrete yet infinite state space. One-counter automata are obtained by extending classical finite-state automata with a counter whose value can range over non-negative integers and be tested for zero. The updates and tests can be further made parametric by introducing a set of integer-valued variables called parameters. The LTL parameter-synthesis problem asks whether a valuation of the parameters exists such that all runs of the automaton satisfy an LTL specification. In this work, we show that (i) this problem is encodable into a decidable restriction of Presburger Arithmetic with Divisibility (PAD), (ii) the parameter synthesis problem is decidable, and in 3NEXP; (iii) the problem is in EXPSPACE where parameters can only be used in counter tests. |
| |
|
Language
|
|
|
|
English
| |
|
Publication
|
|
|
|
Antwerp
:
The University of Antwerp & The University of Bordeaux
,
2023
| |
|
Volume/pages
|
|
|
|
xviii, 136 p.
| |
|
Note
|
|
|
|
:
Fijalkow, Nathanaël [Supervisor]
:
Pérez, Guillermo [Supervisor]
:
Lerôux, Jérome [Supervisor]
| |
|
Full text (open access)
|
|
|
|
| |
|