1,720,981 research outputs found
Model Checking of Optimal LTL and ASAP Properties
No full textModel checking has long been employed as a method for the formal verification of control systems, with a focus on ensuring correctness and safety. However, in practical scenarios (e.g., robotics, aviation and aerospace), simply verifying whether a control system satisfies a given property may not suffice. There is often the requisite to optimize system behavior with respect to certain criteria, such as response time. For instance, in verifying a reachability property, one may be interested in knowing if the controller reaches the goal as soon as possible (ASAP). Despite the simplicity of such requirement, its formalization has not yet been addressed in the literature and requires to reason about the strategy of the controller and the cost of the executions in closed-loop with the given environment. More in general, this paper proposes the formalization and verification of properties for controllers that must satisfy a temporal logic specification optimally, i.e., in the best way possible given the behavior on the plant to be controlled. This relies on and is parametrized by a quantitative semantics for temporal logic. We focus on linear-time temporal logic (LTL), for which various quantitative semantics have been defined. In order to characterize the fulfillment of LTL properties as soon as possible (ASAP), we introduce a new quantitative semantics related to the length of the shortest informative prefix. Finally, we focus on ASAP co-safety properties and reduce the optimal model checking to standard qualitative reactive synthesis. We provide a proof of concept demonstration of the reduction with nuXmv
Fairness, Assumptions, and Guarantees for Extended Bounded Response LTL+P Synthesis
No full textRealizability and reactive synthesis from temporal logics are fundamental problems in the formal verification field. The complexity of the Linear-time Temporal Logic with Past (LTL+P) case led to the definition of fragments with lower complexities and simpler algorithms. Recently, the logic of Extended Bounded Response LTL+P (LTLEBR+ P ) has been introduced. It allows one to express any safety language definable in LTL and it is provided with an efficient, fully-symbolic algorithm for reactive synthesis. In this paper, we extend LTLEBR+ P with fairness conditions, assumptions, and guarantees. The resulting logic, called GR-EBR, preserves the main strength of LTLEBR+ P, that is, efficient realizability, and makes it possible to specify properties beyond safety. We study the problem of reactive synthesis for GR-EBR and devise a fully-symbolic algorithm that reduces it to a number of safety subproblems. To ensure soundness and completeness, we propose a general framework for safety reductions in the context of realizability of (fragments of) LTL+P. The experimental evaluation shows the feasibility of the approach
A FIRST-ORDER LOGIC CHARACTERIZATION OF SAFETY AND CO-SAFETY LANGUAGES
Full text linkLinear Temporal Logic (LTL) is one of the most popular temporal logics and comes into play in a variety of branches of computer science. Among the various reasons of its widespread use there are its strong foundational properties: LTL is equivalent to counter-free ω-automata, to star-free ω-regular expressions, and (by Kamp’s theorem) to the First-Order Theory of Linear Orders (FO-TLO). Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not belong or belongs to the language, respectively, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis for LTL. Safety-LTL (resp., coSafety-LTL) is a fragment of LTL where only the tomorrow, the weak tomorrow and the until temporal modalities (resp., the tomorrow, the weak tomorrow and the release temporal modalities) are allowed, that recognises safety (resp., co-safety) languages only. The main contribution of this paper is the introduction of a fragment of FO-TLO, called Safety-FO, and of its dual coSafety-FO, which are expressively complete with respect to the LTL-definable safety and co-safety languages. We prove that they exactly characterize Safety-LTL and coSafety-LTL, respectively, a result that joins Kamp’s theorem, and provides a clearer view of the characterization of (fragments of) LTL in terms of first-order languages. In addition, it gives a direct, compact, and self-contained proof that any safety language definable in LTL is definable in Safety-LTL as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow operator of Safety-LTL, interpreted over finite and infinite words. Moreover, we prove that, when interpreted over finite words, Safety-LTL (resp. coSafety-LTL) devoid of the tomorrow (resp., weak tomorrow) operator captures the safety (resp., co-safety) fragment of LTL over finite words. We then investigate some formal properties of Safety-FO and coSafety-FO: (i) we study their succinctness with respect to their modal counterparts, namely, Safety-LTL and coSafety-LTL; (ii) we illustrate an important practical application of them in the context of reactive synthesis; (iii) we compare them with expressively equivalent first-order fragments. Last but not least, we provide different characterizations of the (co-)safety fragment of LTL in terms of temporal logics, automata, and regular expressions
Extended bounded response LTL: a new safety fragment for efficient reactive synthesis
No full textReactive synthesis is a key technique for the design of correct-by-construction systems, which has been thoroughly investigated in the last decades. It consists of the synthesis of a controller that reacts to environment’s inputs satisfying a given temporal logic specification. Common approaches are based on the explicit construction of automata and on their determinization, which limits their scalability. In this paper, we introduce a new safety fragment of Linear Temporal Logic (LTL), called Extended Bounded Response LTL (LTLEBR), which allows one to combine bounded and universal unbounded temporal operators (thus covering a large set of practical cases). We show that reactive synthesis from LTLEBR specifications can be reduced to solving a safety game over a deterministic symbolic automaton built directly from the specification. We prove the correctness of the approach and study the complexity of the fragment showing that the proposed solution is optimal. Finally, we evaluate it on various benchmarks showing better performance of other approaches for general LTL or larger safety fragments
Set-Based Invariants over Polynomial Systems
Full text linkDynamical systems model the time evolution of both natural and engineered processes. The automatic analysis of such models relies on different techniques ranging from reachability analysis, model checking, theorem proving, and abstractions. In this context, invariants are subsets of the state space containing all the states reachable from themself. The verification and synthesis of invariants is still a challenging problem over many classes of dynamical systems, since it involves the analysis of an infinite time horizon. In this paper we propose a method for computing invariants through sets of trajectories propagation. The method has been implemented and tested in the tool Sapo which provides reachability methods over discrete time polynomial dynamical systems
Safe decomposition of startup requirements: verification and synthesis
No full textThe initialization of complex cyber-physical systems often requires the interaction of various components that must start up with strict timing requirements on the provision of signals (power, refrigeration, light, etc.). In order to safely allow an independent development of components, it is necessary to ensure a safe decomposition, i.e. the specification of local timing requirements that prevent later integration errors due to the dependencies. We propose a high-level formalism to model local timing requirements and dependencies. We consider the problem of checking the consistency (existence of an execution satisfying the requirements) and compatibility (absence of an execution that reaches an integration error) of the local requirements, and the problem of synthesizing a region of timing constraints that represents all possible correct refinements of the original specification. We show how the problems can be naturally translated into a model checking and synthesis problem for timed automata with shared variables. Exploiting the linear structure of the requirements, we propose an encoding of the problem into SMT. We evaluate the SMT-based approach using MathSAT and show how it scales better than the automata-based approach using Uppaal and nuXmv
GR(1) is equivalent to R(1)
No full textThe organization of temporal properties into a Temporal Hierarchy proposed by Manna and Pnueli is central in the study of the expressive power of fragments of Linear Temporal Logic with Past (LTL+P). A crucial role is played by the Reactivity class, which itself forms a hierarchy consisting of the classes Reactivity(1), Reactivity(2), and so on, and it is proved to be expressively equivalent to LTL+P. The logic of Generalized Reactivity(1) (GR(1) for short), introduced in the context of reactive synthesis, expands the Reactivity(1) class (abbreviated R(1)) with safety formulas and multiple fairness conditions. In this paper, we prove that GR(1) is expressively equivalent to R(1). We first define a simple normal form for GR(1) formulas, and then we prove the expressive equivalence between GR(1) (in such a normal form) and R(1). In addition, we show that all the involved translations require only a linear increase in size. Finally, we lift these results to the general case proving that GR(N) is equivalent to R(N), for all N≥1
Fairness, assumptions, and guarantees for extended bounded response LTL+P synthesis
Full text linkRealizability and reactive synthesis from temporal logics are fundamental problems in formal verification. The complexity of these problems for linear temporal logic with past (LTL+P) led to the identification of fragments with lower complexities and simpler algorithms. Recently, the logic of extended bounded response LTL+P (LTLEBR+ P for short) has been introduced. It allows one to express safety languages definable in LTL+P and it is provided with an efficient, fully symbolic algorithm for reactive synthesis. This paper features four related contributions. First, we introduce GR-EBR , an extension of LTLEBR+ P with fairness conditions, assumptions, and guarantees that, on the one hand, allows one to express properties beyond the safety fragment and, on the other, it retains the efficiency of LTLEBR+ P in practice. Second, we the expressiveness of GR-EBR starting from the expressiveness of its fragments. In particular, we prove that: (1) LTLEBR+ P is expressively complete with respect to the safety fragment of LTL+P , (2) the removal of past operators from LTLEBR+ P results into a loss of expressive power, and (3) GR-EBR is expressively equivalent to the logic GR(1) of Bloem et al. Third, we provide a fully symbolic algorithm for the realizability problem from GR-EBR specifications, that reduces it to a number of safety subproblems. Fourth, to ensure soundness and completeness of the algorithm, we propose and exploit a general framework for safety reductions in the context of realizability of (fragments of) LTL+P . The experimental evaluation shows promising results
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
- …
