Related papers: Truly On-The-Fly LTL Model Checking
This work considers the path planning problem for a team of identical robots evolving in a known environment. The robots should satisfy a global specification given as a Linear Temporal Logic (LTL) formula over a set of regions of interest.…
Consider a discrete dynamical system given by a square matrix $M \in \mathbb{Q}^{d \times d}$ and a starting point $s \in \mathbb{Q}^d$. The orbit of such a system is the infinite trajectory $\langle s, Ms, M^2s, \ldots\rangle$. Given a…
Both automatic program verification and program transformation are based on program analysis. In the past decade a number of approaches using various automatic general-purpose program transformation techniques (partial deduction,…
The use of temporal logics has long been recognised as a fundamental approach to the formal specification and verification of reactive systems. In this paper, we take on the problem of automatically verifying a temporal property, given by a…
We propose an automated method for checking the validity of a formula of HFL(Z), a higher-order logic with fixpoint operators and integers. Combined with Kobayashi et al.'s reduction from higher-order program verification to HFL(Z) validity…
Virtually all verification and synthesis techniques assume that the formal specifications are readily available, functionally correct, and fully match the engineer's understanding of the given system. However, this assumption is often…
We propose a novel adaptive reinforcement learning control approach for fault tolerant control of degrading systems that is not preceded by a fault detection and diagnosis step. Therefore, \textit{a priori} knowledge of faults that may…
One clock alternating timed automata (OCATA) have been introduced as natural extension of (one clock) timed automata to express the semantics of MTL. In this paper, we consider the application of OCATA to the problems of model-checking and…
Given a deterministic finite automaton and its implementation with at most one single fault, that we can test on a set of inputs, we provide an algorithm to find a test set that guarantees finding whether the fault exists.
It is important to find optimal solutions for structural errors in rule-based expert systems .Solutions to discovering such errors by using model checking techniques have already been proposed, but these solutions have problems such as…
Since the introduction of Alternating-time Temporal Logic (ATL), many logics have been proposed to reason about different strategic capabilities of the agents of a system. In particular, some logics have been designed to reason about the…
In the field of robotics, researchers face a critical challenge in ensuring reliable and efficient task planning. Verifying high-level task plans before execution significantly reduces errors and enhance the overall performance of these…
While automated driving technology has achieved a tremendous progress, the scalable and rigorous testing and verification of safe automated and autonomous driving vehicles remain challenging. This paper proposes a learning-based…
This 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,…
Model checking of temporal logics in a well established technique to verify and validate properties of multi-agent systems (MAS). However, practical model checking requires input models of manageable size. In this paper, we extend the model…
A key challenge in formal verification, particularly in Model Checking, is ensuring the correctness of the verification tools. Erroneous results on complex models can be difficult to detect, yet a high level of confidence in the outcome is…
A notion of alternating timed automata is proposed. It is shown that such automata with only one clock have decidable emptiness problem over finite words. This gives a new class of timed languages which is closed under boolean operations…
Propositional Projection Temporal Logic (PPTL) is a useful formalism for reasoning about period of time in hardware and software systems and can handle both sequential and parallel compositions. In this paper, based on discrete time Markov…
We present a knowledge compilation approach for existential and universal quantification in alternating automata. Knowledge compilation transforms formulas into normal forms with special properties that enable efficient answering of…
The model-checking problem for probabilistic systems crucially relies on the translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless translation for the LTL(F,G) fragment produces smaller automata as compared to the…