Related papers: Improving HyLTL model checking of hybrid systems
Parametric timed automata extend timed automata (Alur and Dill, 1991) in that they allow the specification of parametric bounds on the clock values. Since their introduction in 1993 by Alur, Henzinger, and Vardi, it is known that the…
Synthesis of models and strategies is a very important problem in software engineering. The main element here is checking the satisfiability of formulae expressing the specification of a system to be implemented. This paper puts forward a…
This article introduces a fully automated verification technique that permits to analyze real-time systems described using a continuous notion of time and a mixture of operational (i.e., automata-based) and descriptive (i.e., logic-based)…
We study the satisfiability and model-checking problems for timed hyperproperties specified with HyperMTL, a timed extension of HyperLTL. Depending on whether interleaving of events in different traces is allowed, two possible semantics can…
HyperLTL is an extension of linear-time temporal logic for the specification of hyperproperties, i.e., temporal properties that relate multiple computation traces. HyperLTL can express information flow policies as well as properties like…
Path checking, the special case of the model checking problem where the model under consideration is a single path, plays an important role in monitoring, testing, and verification. We prove that for linear-time temporal logic (LTL), path…
We consider the problem of the verification of an LTL specification $\varphi$ on a system $S$ given some prior knowledge $K$, an LTL formula that $S$ is known to satisfy. The automata-theoretic approach to LTL model checking is implemented…
Synthesizing a reactive system from specifications given in linear temporal logic (LTL) is a classical problem, finding its applications in safety-critical systems design. These systems are typically represented using either Mealy machines…
Multi-valued logics have a long tradition in the literature on system verification, including run-time verification. However, comparatively fewer model-checking tools have been developed for multi-valued specification languages. We present…
There have been several recent suggestions for tableau systems for deciding satisfiability in the practically important branching time temporal logic known as CTL*. In this paper we present a streamlined and more traditional tableau…
We discuss the problem of experimentally evaluating linear-time temporal logic (LTL) synthesis tools for reactive systems. We first survey previous such work for the currently publicly available synthesis tools, and then draw conclusions by…
We revisit a fundamental result in real-time verification, namely that the binary reachability relation between configurations of a given timed automaton is definable in linear arithmetic over the integers and reals. In this paper we give a…
We introduce a functional inductive framework to verify discrete-time dynamical systems against hyperproperties specified as Hyperlinear temporal logic formulae via a notion of HyperCertificates. Unlike linear temporal logic (LTL) formulae…
Bounded model checking (BMC) is an effective technique for hunting bugs by incrementally exploring the state space of a system. To reason about infinite traces through a finite structure and to ultimately obtain completeness, BMC…
Research in robotic planning with temporal logic specifications, such as Linear Temporal Logic (LTL), has relied on single formulas. However, as task complexity increases, LTL formulas become lengthy, making them difficult to interpret and…
Hybrid systems are mostly modelled, simulated, and verified in the time domain by computer scientists. Engineers, however, use both frequency and time domain modelling due to their distinct advantages. For example, frequency domain…
We address the problem of diagnosing and repairing specifications for hybrid systems formalized in signal temporal logic (STL). Our focus is on the setting of automatic synthesis of controllers in a model predictive control (MPC) framework.…
We consider multi-robot systems under recurring tasks formalized as linear temporal logic (LTL) specifications. To solve the planning problem efficiently, we propose a bottom-up approach combining offline plan synthesis with online…
Higher-Order Fixpoint Logic (HFL) is a hybrid of the simply typed \lambda-calculus and the modal \lambda-calculus. This makes it a highly expressive temporal logic that is capable of expressing various interesting correctness properties of…
In many multirobot applications, planning trajectories in a way to guarantee that the collective behavior of the robots satisfies a certain high-level specification is crucial. Motivated by this problem, we introduce counting temporal…