Being Correct Is Not Enough: Efficient Verification Using Robust Linear Temporal Logic

While most approaches in formal methods address system correctness, ensuring robustness has remained a challenge. In this article, we present and study the logic rLTL, which provides a means to formally reason about both correctness and robustness in system design. Furthermore, we identify a large fragment of rLTL for which the verification problem can be efficiently solved, i.e., verification can be done by using an automaton, recognizing the behaviors described by the rLTL formula φ, of size at most O(3 |φ |), where |φ | is the length of φ. This result improves upon the previously known bound of O(5|φ |) for rLTL verification and is closer to the LTL bound of O(2|φ |). The usefulness of this fragment is demonstrated by a number of case studies showing its practical significance in terms of expressiveness, the ability to describe robustness, and the fine-grained information that rLTL brings to the process of system verification. Moreover, these advantages come at a low computational overhead with respect to LTL verification.

Automatic simulation-based testing of autonomous ships using Gaussian processes and temporal logic

A methodology for automatic simulation-based testing of control systems for autonomous vessels is proposed. The work is motivated by the need for increased test coverage and formalism in the verification efforts. It aims to achieve this by formulating requirements in the formal logic Signal Temporal Logic (STL). This enables automatic evaluation of simulations against requirements using the STL robustness metric, resulting in a robustness score for requirements satisfaction. Furthermore, the proposed method uses a Gaussian Process (GP) model for estimating robustness scores including levels of uncertainty for untested cases. The GP model is updated by running simulations and observing the resulting robustness, and its estimates are used to automatically guide the test case selection toward cases with low robustness or high uncertainty. The main scientific contribution is the development of an automatic testing method which incrementally runs new simulations until the entire parameter space of the case is covered to the desired confidence level, or until a case which falsifies the requirement is identified. The methodology is demonstrated through a case study, where the test object is a Collision Avoidance (CA) system for a small high-speed vessel. STL requirements for safety distance, mission compliance, and COLREG compliance are developed. The proposed method shows promise, by both achieving verification in feasible time and identifying falsifying behaviors which would be difficult to detect manually or using brute-force methods. An additional contribution of this work is a formalization of COLREG using temporal logic, which appears to be an interesting direction for future work.

Linear-Time Temporal Answer Set Programming

In this survey, we present an overview on (Modal) Temporal Logic Programming in view of its application to Knowledge Representation and Declarative Problem Solving. The syntax of this extension of logic programs is the result of combining usual rules with temporal modal operators, as in Linear-time Temporal Logic (LTL). In the paper, we focus on the main recent results of the non-monotonic formalism called Temporal Equilibrium Logic (TEL) that is defined for the full syntax of LTL but involves a model selection criterion based on Equilibrium Logic, a well known logical characterization of Answer Set Programming (ASP). As a result, we obtain a proper extension of the stable models semantics for the general case of temporal formulas in the syntax of LTL. We recall the basic definitions for TEL and its monotonic basis, the temporal logic of Here-and-There (THT), and study the differences between finite and infinite trace length. We also provide further useful results, such as the translation into other formalisms like Quantified Equilibrium Logic and Second-order LTL, and some techniques for computing temporal stable models based on automata constructions. In the remainder of the paper, we focus on practical aspects, defining a syntactic fragment called (modal) temporal logic programs closer to ASP, and explaining how this has been exploited in the construction of the solver telingo, a temporal extension of the well-known ASP solver clingo that uses its incremental solving capabilities.

Unbounded Model Checking for ATL

In this paper, we deal with verification of multi-agent systems represented as concurrent game structures. To express properties to be verified, we use Alternating-Time Temporal Logic (ATL) formulas. We provide an implementation of symbolic model checking for ATL and preliminary, but encouraging experimental results.

Incremental execution of temporal graph queries over runtime models with history and its applications

Modern software systems are intricate and operate in highly dynamic environments for which few assumptions can be made at design-time. This setting has sparked an interest in solutions that use a runtime model which reflects the system state and operational context to monitor and adapt the system in reaction to changes during its runtime. Few solutions focus on the evolution of the model over time, i.e., its history, although history is required for monitoring temporal behaviors and may enable more informed decision-making. One reason is that handling the history of a runtime model poses an important technical challenge, as it requires tracing a part of the model over multiple model snapshots in a timely manner. Additionally, the runtime setting calls for memory-efficient measures to store and check these snapshots. Following the common practice of representing a runtime model as a typed attributed graph, we introduce a language which supports the formulation of temporal graph queries, i.e., queries on the ordering and timing in which structural changes in the history of a runtime model occurred. We present a querying scheme for the execution of temporal graph queries over history-aware runtime models. Features such as temporal logic operators in queries, the incremental execution, the option to discard history that is no longer relevant to queries, and the in-memory storage of the model, distinguish our scheme from relevant solutions. By incorporating temporal operators, temporal graph queries can be used for runtime monitoring of temporal logic formulas. Building on this capability, we present an implementation of the scheme that is evaluated for runtime querying, monitoring, and adaptation scenarios from two application domains.

Undecidability of QLTL with two variables and one monadic predicate letter

We study the algorithmic properties of the quantified linear-time temporal logic QLTL in languages with restrictions on the number of individual variables as well as the number and arity of predicate letters. We prove that the satisfiability problem for QLTL in languages with two individual variables and one monadic predicate letter in Σ 11 -hard. Thus, QLTL is Π 11 -hard, and so not recursively enumerable, in such languages. The resultholds both for the increasing domain and the constant domain semantics and is obtained by reduction from a Σ 11 -hard N×N recurrent tiling problem. It follows from the proof for QLTL that similar results hold for the quantified branching-time temporal logic QCTL, and hence for the quantified alternating-time temporal logic QATL. The result presented in this paper strengthens a result by I. Hodkinson, F. Wolter, and M. Zakharyaschev, who have shown that the satisfiability problem for QLTL is Σ 11 -hard in languages with two individual variablesand an unlimited supply of monadic predicate letters.

On the Satisfiability and Model Checking for one Parameterized Extension of Linear-time Temporal Logic

Sequential reactive systems are computer programs or hardware devices which process the flows of input data or control signals and output the streams of instructions or responses. When designing such systems one needs formal specification languages capable of expressing the relationships between the input and output flows. Previously, we introduced a family of such specification languages based on temporal logics $LTL$, $CTL$ and $CTL^*$ combined with regular languages. A characteristic feature of these new extensions of conventional temporal logics is that temporal operators and basic predicates are parameterized by regular languages. In our early papers, we estimated the expressive power of the new temporal logic $Reg$-$LTL$ and introduced a model checking algorithm for $Reg$-$LTL$, $Reg$-$CTL$, and $Reg$-$CTL^*$. The main issue which still remains unclear is the complexity of decision problems for these logics. In the paper, we give a complete solution to satisfiability checking and model checking problems for $Reg$-$LTL$ and prove that both problems are Pspace-complete. The computational hardness of the problems under consideration is easily proved by reducing to them the intersection emptyness problem for the families of regular languages. The main result of the paper is an algorithm for reducing the satisfiability of checking $Reg$-$LTL$ formulas to the emptiness problem for Buchi automata of relatively small size and a description of a technique that allows one to check the emptiness of the obtained automata within space polynomial of the size of input formulas.