1,720,987 research outputs found
Temporal Logic Specifications: Expressiveness, Satisfiability and Realizability
Full text linkL’argomento principale di questa tesi riguarda le logiche temporali, con particolare attenzione alla loro potenza espressiva e ai problemi di soddisfacibilità e realizzabilità.
Le logiche temporali sono oggigiorno un formalismo ben consolidato per esprimere proprietà su sequenze. La loro connessione con logiche al primo e second’ordine, con gli automi e con la verifica formale ha reso le logiche temporali non solo un potente framework teorico, ma anche un prezioso strumento pratico (per esempio per la specifica di sistemi concorrenti). Sul lato teorico, uno dei tipici problemi quando si lavora con una logica temporale è di caratterizzare esattamente la sua potenza espressiva, cioè di dare l’insieme di tutte e sole le proprietà che essa è in grado di formalizzare. Su un lato più pratico, ci sono due importanti problemi che vengono considerati quando si usano le logiche temporali come linguaggi di specifica: (i) il problema di soddisfacibilità, cioè stabilire se la formula data ammette almeno un modello; e (ii) il problema di realizzabilità, cioè stabilire se la formula data è implementabile. In verifica formale, la soddisfacibilità può essere usata come un controllo per individuare specifiche vacue (cioè formule valide o insoddisfacibili), mentre la realizzabilità può essere usata per controllare l’esistenza di implementazioni corrette per costruzione (e la loro conseguente sintesi).
In questa tesi, cerchiamo di porci nell’intersezione tra il lato teorico e quello pratico delle logiche temporali, accompagnando i risultati teorici (quando possibile) con algoritmi, implementazioni e valutazioni sperimentali.
Teoria: Introduciamo tre frammenti della Logica Temporale Lineare con Passato (LTL+P) e studiamo la loro potenza espressiva:
(i) per il primo frammento (chiamato LTLEBR+P) dimostriamo che è espressivamente completo rispetto al frammento safety semantico di LTL+P (una proprietà si dice essere di safety se ogni sua violazione è irrimediabile); (ii) il secondo frammento (chiamato LTLEBR) è ottenuto da LTLEBR+P rimuovendo gli operatori al passato; dimostriamo che LTLEBR è strettamente meno espressivo di LTLEBR+P (iii) il terzo frammento `e chiamato GR-EBR ed è un’estensione di LTLEBR+P per esprimere proprietà che vanno oltre al frammento safety; confrontiamo la sua potenza espressiva con la Temporal Hierarchy di Manna e Pnueli. Inoltre proponiamo una caratterizzazione sintattica al prim’ordine (chiamata Safety-FO) che cattura il frammento safety semantico della logica al prim’ordine con un successore: questo risultato può essere considerato come la versione del Teorema di Kamp per proprietà safety.
Problemi e Algoritmi: Consideriamo il problema di soddisfacibilità per LTL+P ed il problema di realizzabilità per specifiche di LTLEBR+P e GR-EBR. Particolare attenzione è rivolta all’uso di algoritmi simbolici al posto di quelli classici espliciti. Implementiamo tutti gli algoritmi che abbiamo proposto e li confrontiamo con gli altri tool concorrenti. Dai risultati delle valutazioni sperimentali, è spesso evidente che le nostre tecniche simboliche riescono a risolvere istanze di dimensioni che sono proibitive per gli altri tool basati su una rappresentazione esplicita.
Ultimo, ma non per importanza, consideriamo un problema di rilevanza industriale nel contesto di requisiti real-time (cioè proprietà che esprimono non solo l’ordine tra gli eventi ma anche la quantità di tempo passata tra i due). Definiamo e formalizziamo il problema di compatibilità di requisiti temporizzati, diamo degli algoritmi simbolici per questo problema, e implementiamo e valutiamo la procedura proposta.The main topic of this thesis concerns temporal logics, with particular attention to their expressive power and to the satisfiability and realizability problems.
Temporal logics are nowadays a well-established formalism for expressing properties about sequences. Their connection with first- and second-order logic, automata and formal verification makes temporal logics not only a powerful theoretical framework, but also a valuable tool in practical scenarios (e.g., for the specification of con- current systems). On the theoretical side, one typical problem when dealing with a temporal logic is to characterize exactly its expressive power, that is to give the set of all and only the properties that it can formalize. On a more practical side, there are two important problems that are considered when using temporal logics as specification languages: (i) the satisfiability problem, that is finding whether a given formula admits at least one model; and (ii) the realizability problem, namely to find whether a given formula is implementable. In formal verification, satisfiability can be used as a sanity check for detecting vacuous specifications (i.e., valid or unsatisfiable formulas), while realizability can be used to check the existence of correct-by-construction implementations (and their consequent synthesis).
In this thesis, we try to stay in the intersection between the theoretical and the practical sides of temporal logics, by accompanying the theoretical results (whenever possible) with algorithms, implementations and experimental evaluations.
Theory: We introduce three fragments of Linear Temporal Logic with Past (LTL+P) and study their expressive power: (i) for the first fragment (called LTLEBR+P), we prove that it is expressively complete with respect to the (semantically) safety fragment of LTL+P (a safety property is a property in which a violation is irremediable); (ii) the second fragment (called LTLEBR) is obtained from LTLEBR+P by removing past operators; we prove that LTLEBR is strictly less expressive than full LTLEBR+P; (iii) the third fragment is called GR-EBR and it is an extension of LTLEBR+P for expressing properties beyond the safety fragment; we compare its expressive power with the Temporal Hierarchy of Manna and Pnueli. In addition we propose a first-order syntactical characterization (called Safety-FO) that captures the semantically safety fragment of the first-order logic of one successor: this result can be considered as the version of Kamp’s Theorem for safety properties.
Problems and Algorithms: We consider the satisfiability problem of LTL+P and the realizability problem from LTLEBR+P and GR-EBR specifications. Particular attention is devoted to the use of symbolic algorithms instead of classical explicit-state ones. We implement all the algorithms that we propose and we compare them with competitor tools. From the outcomes of the experimental evaluations, it is often evident that our symbolic techniques can solve instances of sizes that are prohibitive for the other tools based on an explicit-state representation.
Last but not least, we consider an industrially relevant problem in the context of real-time requirements (i.e., properties expressing not only the ordering between events but also the amount of time elapsed between two events). We define and formalize the compatibility problem of timed requirements, give symbolic algorithms for this problem, and implement and evaluate the proposed procedure
Learning What to Monitor: Using Machine Learning to Improve past STL Monitoring
No full textMonitoring is a runtime verification technique that can be used to check whether an execution of a system (trace) satisfies or not a given set of properties. Compared to other formal verification techniques, eg, model checking, one needs to specify the properties to be monitored, but a complete model of the system is no longer necessary. First, we introduce the pure past fragment of Signal Temporal Logic (ppSTL), and we use it to define the monitorable safety (G (ppSTL)) and cosafety (F (ppSTL)) fragments of STL, which properly extend the commonly-used bounded-future fragment. Then, we devise a multi-objective genetic programming algorithm to automatically extend the set of properties to monitor on the basis of the history of failure traces collected over time. The framework resulting from the integration of the monitor and the learning algorithm is then experimentally validated on various public datasets. The outcomes of the experimentation confirm the effectiveness of the proposed solution
Linear Temporal Logic Modulo Theories over Finite Traces
No full textThis paper studies Linear Temporal Logic over Finite Traces (LTLf) where proposition letters are replaced with first-order formulas interpreted over arbitrary theories, in the spirit of Satisfiability Modulo Theories. The resulting logic, called LTLf Modulo Theories (LTLfMT), is semi-decidable. Nevertheless, its high expressiveness comes useful in a number of use cases, such as model-checking of data-aware processes and data-aware planning. Despite the general undecidability of these problems, being able to solve satisfiable instances is a compromise worth studying. After motivating and describing such use cases, we provide a sound and complete semi-decision procedure for LTLfMT based on the SMT encoding of a one-pass tree-shaped tableau system. The algorithm is implemented in the BLACK satisfiability checking tool, and an experimental evaluation shows the feasibility of the approach on novel benchmarks.</jats:p
A SAT-Based Encoding of the One-Pass and Tree-Shaped Tableau System for LTL
Full text linkA new one-pass and tree-shaped tableau system for LTL sat- isfiability checking has been recently proposed, where each branch can be explored independently from others and, furthermore, directly cor- responds to a potential model of the formula. Despite its simplicity, it proved itself to be effective in practice. In this paper, we provide a SAT-based encoding of such a tableau system, based on the technique of bounded satisfiability checking. Starting with a single-node tableau, i.e., depth k of the tree-shaped tableau equal to zero, we proceed in an incremental fashion. At each iteration, the tableau rules are encoded in a Boolean formula, representing all branches of the tableau up to the current depth k. A typical downside of such bounded techniques is the effort needed to understand when to stop incrementing the bound, to guarantee the completeness of the procedure. In contrast, termination and completeness of the proposed algorithm is guaranteed without com- puting any upper bound to the length of candidate models, thanks to the Boolean encoding of the PRUNE rule of the original tableau system. We conclude the paper by describing a tool that implements our procedure, and comparing its performance with other state-of-the-art LTL solvers
Synthesis of Timeline-Based Planning Strategies Avoiding Determinization
No full textQualitative timeline-based planning models domains as sets of independent, but interacting, components whose behaviors over time, the timelines, are governed by sets of qualitative temporal constraints (ordering relations), called synchronization rules. Its plan-existence problem has been shown to be PSPAC[-complete; in particular, PSPAC[-membership has been proved via reduction to the nonemptiness problem for nondeterministic finite automata. However, nondeterministic automata cannot be directly used to synthesize planning strategies as a costly determinization step is needed. In this paper, we identify a large fragment of qualitative timeline-based planning whose plan-existence problem can be directly mapped into the nonemptiness problem of deterministic finite automata, which can then be exploited to synthesize strategies. In addition, we identify a maximal subset of Allen's relations that fits into such a deterministic fragment
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, that
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 omega-automata, to star-free omega-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. SafetyLTL (resp., coSafetyLTL)
is a fragment of LTL where only universal (resp., existential) 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 SafetyFO, and of its dual coSafetyFO, which are expressively
complete with respect to the LTL-definable safety and co-safety languages. We
prove that they exactly characterize SafetyLTL and coSafetyLTL, 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 SafetyLTL as well. As a by-product,
we obtain some interesting results on the expressive power of the weak tomorrow
operator of SafetyLTL, interpreted over finite and infinite words. Moreover, we
prove that, when interpreted over finite words, SafetyLTL (resp. coSafetyLTL)
devoid of the tomorrow (resp., weak tomorrow) operator captures the safety
(resp., co-safety) fragment of LTL over finite words
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
- …
