Efficient Runtime Verification of First-Order Temporal Properties

2018 ◽  
pp. 26-47 ◽  
Author(s):  
Klaus Havelund ◽  
Doron Peled
Keyword(s):  
Runtime Verification ◽  
First Order ◽  
Temporal Properties

Event-Based Runtime Verification of Temporal Properties Using Time Basic Petri Nets

2017 ◽  
pp. 115-130 ◽  
Author(s):  
Matteo Camilli ◽  
Angelo Gargantini ◽  
Patrizia Scandurra ◽  
Carlo Bellettini
Keyword(s):  
Petri Nets ◽  
Runtime Verification ◽  
Temporal Properties ◽  
Event Based

The ins and outs of first-order runtime verification

2015 ◽  
Vol 46 (3) ◽  
pp. 286-316 ◽  
Author(s):  
Andreas Bauer ◽  
Jan-Christoph Küster ◽  
Gil Vegliach
Keyword(s):  
Runtime Verification ◽  
First Order

scholarly journals VERIFICATION OF CONJUNCTIVE ARTIFACT-CENTRIC SERVICES

2012 ◽  
Vol 21 (02) ◽  
pp. 111-139 ◽  
Author(s):  
GIUSEPPE DE GIACOMO ◽  
RICCARDO DE MASELLIS ◽  
RICCARDO ROSATI
Keyword(s):  
Relational Database ◽  
Data Exchange ◽  
Recent Literature ◽  
Conjunctive Queries ◽  
First Order ◽  
Temporal Properties ◽  
Verification Time

An artifact-centric service is a stateful service that holistically represents both the data and the process in terms of a (dynamic) artifact. An artifact is constituted by a data component, holding all the data of interest for the service, and a lifecycle, which specifies the process that the service enacts. In this paper, we study artifact-centric services whose data component is a full-fledged relational database, queried through (first-order) conjunctive queries, and the lifecycle component is specified as sets of condition-action rules, where actions are tasks invocations, again based on conjunctive queries. Notably, the database can evolve in an unbounded way due to new values (unknown at verification time) inserted by tasks. The main result of the paper is that verification in this setting is decidable under a reasonable restriction on the form of tasks, called weak acyclicity, which we borrow from the recent literature on data exchange. In particular, we develop a sound, complete and terminating verification procedure for sophisticated temporal properties expressed in a first-order variant of μ-calculus.

scholarly journals Temporal prophecy for proving temporal properties of infinite-state systems

2021 ◽  
Author(s):  
Oded Padon ◽  
Jochen Hoenicke ◽  
Kenneth L. McMillan ◽  
Andreas Podelski ◽  
Mooly Sagiv ◽  
...  
Keyword(s):  
Order Logic ◽  
Cut Elimination ◽  
Temporal Property ◽  
Deductive Verification ◽  
First Order ◽  
Temporal Properties ◽  
Safety Property ◽  
Infinite State Systems ◽  
Verification Techniques ◽  
Infinite State

AbstractVarious verification techniques for temporal properties transform temporal verification to safety verification. For infinite-state systems, these transformations are inherently imprecise. That is, for some instances, the temporal property holds, but the resulting safety property does not. This paper introduces a mechanism for tackling this imprecision. This mechanism, which we call temporal prophecy, is inspired by prophecy variables. Temporal prophecy refines an infinite-state system using first-order linear temporal logic formulas, via a suitable tableau construction. For a specific liveness-to-safety transformation based on first-order logic, we show that using temporal prophecy strictly increases the precision. Furthermore, temporal prophecy leads to robustness of the proof method, which is manifested by a cut elimination theorem. We integrate our approach into the Ivy deductive verification system, and show that it can handle challenging temporal verification examples.

scholarly journals Do You Need Infinite Time?

2019 ◽  
Author(s):  
Alessandro Artale ◽  
Andrea Mazzullo ◽  
Ana Ozaki
Keyword(s):  
Temporal Logic ◽  
Planning Process ◽  
Description Logics ◽  
Automated Planning ◽  
Linear Temporal Logic ◽  
Runtime Verification ◽  
Process Modelling ◽  
Infinite Time ◽  
First Order ◽  
Temporal Specification

Linear temporal logic over finite traces is used as a formalism for temporal specification in automated planning, process modelling and (runtime) verification. In this paper, we investigate first-order temporal logic over finite traces, lifting some known results to a more expressive setting. Satisfiability in the two-variable monodic fragment is shown to be EXPSPACE-complete, as for the infinite trace case, while it decreases to NEXPTIME when we consider finite traces bounded in the number of instants. This leads to new complexity results for temporal description logics over finite traces. We further investigate satisfiability and equivalences of formulas under a model-theoretic perspective, providing a set of semantic conditions that characterise when the distinction between reasoning over finite and infinite traces can be blurred. Finally, we apply these conditions to planning and verification.

scholarly journals Loop Analysis by Quantification over Iterations

10.29007/269p ◽  
2018 ◽  
Author(s):  
Bernhard Gleiss ◽  
Laura Kovács ◽  
Simon Robillard
Keyword(s):  
Software Verification ◽  
Loop Analysis ◽  
Termination Analysis ◽  
Invariant Generation ◽  
Partial Correctness ◽  
First Order ◽  
Temporal Properties ◽  
Smt Solvers ◽  
Order Language ◽  
Soundness And Completeness

We present a framework to analyze and verify programs containing loops by using a first-order language of so-called extended expressions. This language can express both functional and temporal properties of loops. We prove soundness and completeness of our framework and use our approach to automate the tasks of partial correctness verification, termination analysis and invariant generation. For doing so, we express the loop semantics as a set of first-order properties over extended expressions and use theorem provers and/or SMT solvers to reason about these properties. Our approach supports full first-order reasoning, including proving program properties with alternation of quantifiers. Our work is implemented in the tool QuIt and successfully evaluated on benchmarks coming from software verification.

Sign in / Sign up

Export Citation Format

Share Document