1,721,000 research outputs found
Pushing runtime verification to the limit: May process semantics be with Us
No full textWe propose a combined approach that permits automated formal verification to be spread across the pre- and post-deployment phases of a system development, with the aim of calibrating the management of the verification burden. Our approach combines standard model checking methods with runtime verification, a relatively novel formal technique that verifies a system during its execution. We carry out our study in terms of the Hennessy-Milner Logic, a branching-time logic for specifying reactive system correctness. Whereas we will be mainly concerned with limiting the model checking verification burden, runtime verification has been shown to handle a strict subset of the expressible properties in our logic of study, posing constraints on what can be shifted to the post-deployment phase. We present a solution, based on modal transition systems and modal refinement, for the fragment of the Hennessy-Milner Logic devoid of recursion, i.e., without least and greatest fixpoint operators
Pairing monitoring with machine learning for smart system verification and predictive maintenance
No full textOver the last decades, the advancements in microelectronic technologies allowed for the embedding of complex digital sensors in several systems, ranging from home appliances to health tracking devices and industrial plant machinery. The resulting systems are, in general, quite complex, given the possible heterogeneity of their components and the non-trivial ways in which sensors may interact. In critical domains, formal methods have been employed to ensure the correct behaviour of a system. However, a complete specification of all the properties that have to be guaranteed turns out to be often out of reach, due to the inherent complexity of the system and of its interactions with the environment in which it operates. To overcome these limitations, some approaches that complement formal verification with model-based testing and monitoring have been recently proposed. In this paper, we argue for the opportunity of pairing monitoring with machine learning techniques in order to improve its ability of detecting critical system behaviours
Extended ω-Regular Languages and Interval Temporal Logic
Full text linkSome extensions of ω-regular languages have been proposed in the literature to express asymptotic properties of ω-words which are not captured by ω-regular languages. Formal definitions of extended ωregular languages have been given in terms of both suitable classes of automata and extended ω-regular expressions. On the contrary, satisfactory temporal logic counterparts are still missing. In this paper, we give a characterization of them in terms of interval temporal logics
An interval temporal logic characterization of extended ω-regular languages
No full textSome extensions of ω-regular languages have been proposed in the literature to express asymptotic properties of ω-words which are not captured by ω-regular languages. They include ωB-regular languages, that extend ω-regular languages with boundedness, ωS-regular languages, that enrich ω-regular ones with strong unboundedness, ωBS-regular languages, that combine ωB- and ωS-regular ones, and ωT-regular languages, that include meaningful languages which are not ωBS-regular. Formal definitions of extended ω-regular languages have been given in terms of both suitable classes of automata and extended ω-regular expressions, while satisfactory temporal logic counterparts are still missing. In this paper, we give a characterization of them in terms of interval temporal logics by providing an explicit encoding of expressions into formulas
Alternating (In)Dependence-Friendly Logic
Full text linkHintikka and Sandu originally proposed Independence Friendly Logic ([Formula presented]) as a first-order logic of imperfect information to describe game-theoretic phenomena underlying the semantics of natural language. The logic allows for expressing independence constraints among quantified variables, in a similar vein to Henkin quantifiers, and has a nice game-theoretic semantics in terms of imperfect information games. However, the [Formula presented] semantics exhibits some limitations, at least from a purely logical perspective. It treats the players asymmetrically, considering only one of the two players as having imperfect information when evaluating truth, resp., falsity, of a sentence. In addition, truth and falsity of sentences coincide with the existence of a uniform winning strategy for one of the two players in the semantic imperfect information game. As a consequence, [Formula presented] does admit undetermined sentences, which are neither true nor false, thus failing the law of excluded middle. These idiosyncrasies limit its expressive power to the existential fragment of Second Order Logic ([Formula presented]). In this paper, we investigate an extension of [Formula presented], called Alternating Dependence/Independence Friendly Logic ([Formula presented]), tailored to overcome these limitations. To this end, we introduce a novel compositional semantics, generalising the one based on trumps proposed by Hodges for [Formula presented]. The new semantics (i) allows for meaningfully restricting both players at the same time, (ii) enjoys the property of game-theoretic determinacy, (iii) recovers the law of excluded middle for sentences, and (iv) grants [Formula presented] the full descriptive power of [Formula presented]. We also provide an equivalent Herbrand-Skolem semantics and a game-theoretic semantics for the prenex fragment of [Formula presented], the latter being defined in terms of a determined infinite-duration game that precisely captures the other two semantics on finite structures
Good-for-Game QPTL: An Alternating Hodges Semantics
No full textAn extension of QPTL is considered where functional dependencies among the quantified variables can be restricted in such a way that their current values are independent of the future values of the other variables. This restriction is tightly connected to the notion of behavioral strategies in game-theory and allows the resulting logic to naturally express game-theoretic concepts. Inspired by the work on logics of dependence and independence, we provide a new compositional semantics for QPTL that allows for expressing such functional dependencies among variables. The fragment where only restricted quantifications are considered, called behavioral quantifications, allows for linear-time properties that are satisfiable if and only if they are realisable in the Pnueli-Rosner sense. This fragment can be decided, for both model checking and satisfiability, in 2Exp Time and is expressively equivalent to QPTL, though significantly less succinct
The Logic of Prefixes and Suffixes is Elementary under Homogeneity*
No full textIn this paper, we study the finite satisfiability problem for the logic BE under the homogeneity assumption. BE is the cornerstone of Halpern and Shoham's interval temporal logic, and features modal operators corresponding to the prefix (a.k.a. "Begins") and suffix (a.k.a. "Ends") relations on intervals. In terms of complexity, BE lies in between the "Chop"logic C, whose satisfiability problem is known to be non-elementary, and the PSpace-complete interval logic D of the sub-interval (a.k.a. "During") relation. BE was shown to be ExpSpace-hard, and the only known satisfiability procedure is primitive recursive, but not elementary. Our contribution consists of tightening the complexity bounds of the satisfiability problem for BE, by proving it to be ExpSpace-complete. We do so by devising an equi-satisfiable normal form with boundedly many nested modalities. The normalization technique resembles Scott's quantifier elimination, but it turns out to be much more involved due to the limitations enforced by the homogeneity assumption
The light side of interval temporal logic: The Bernays-Schönfinkel fragment of CDT
No full textDecidability and complexity of the satisfiability problem for the logics of time intervals have been extensively studied in the recent years. Even though most interval logics turn out to be undecidable, meaningful exceptions exist, such as the logics of temporal neighborhood and (some of) the logics of the subinterval relation. In this paper, we explore a different path to decidability: instead of restricting the set of modalities or imposing severe semantic restrictions, we take the most expressive interval temporal logic studied so far, namely, Venema's CDT, and we suitably limit the negation depth of modalities. The decidability of the satisfiability problem for the resulting fragment, called CDT_BS, over the class of all linear orders, is proved by embedding it into a well-known decidable quantifier prefix class of first-order logic, namely, Bernays-Schönfinkel class. In addition, we show that CDT_BS is in fact NP-complete (Bernays-Schönfinkel class is NEXPTIME-complete), and we prove its expressive completeness with respect to a suitable fragment of Bernays-Schönfinkel class. Finally, we show that any increase in the negation depth of CDT_BS modalities immediately yields undecidability
An interval temporal logic characterization of extended ω-regular languages
No full textSome extensions of w-regular languages have been proposed in the literature to express asymptotic properties of w-words which are not captured by w-regular languages. They include wB-regular languages, that extend w-regular languages with boundedness, wS- regular languages, that enrich w-regular ones with strong unboundedness, wBS-regular languages, that combine wB- and wS-regular ones, and wff-regular languages, that include meaningful languages which are not wBS-regular. Formal definitions of extended w-regular languages have been given in terms of both suitable classes of automata and extended w -regular expressions, while satisfactory temporal logic counterparts are still missing. In this paper, we give a characterization of them in terms of interval temporal logics by providing an explicit encoding of expressions into formulas.(c) 2023 Elsevier B.V. All rights reserved
- …
