scholarly journals A logic for synchronous transitions with dynamic conflict resolution

2000 ◽  
Vol 3 (2) ◽  
Author(s):  
Vanderlei Moraes Rodrigues ◽  
Flavio Rech Wagner
Keyword(s):  
Conflict Resolution ◽  
Linear Time ◽  
Transition System ◽  
Temporal Logics ◽  
Computation Model ◽  
Formal Reasoning ◽  
Resolution Method ◽  
Transition Systems ◽  
Synchronous Computation ◽  
Linear Time Temporal Logic

This paper introduces a formalism named DSYNC aimed at. the design and verification of synchronous concurrent systems. The components of this formalism are a transition system and first-order linear-time temporal logic. The DSYNC transition system adopts a synchronous computation model, includes a method to solve write-conflicts, and represents transitions as possibly non-terminating imperative commands. The conflict resolution method is dynamic because it detects conflicts at run-time. The DSYNC logic allows for formal reasoning about DSYNC transition systems using compositional and modular proofs. Such features are missing in other formalisms based on transition systems and temporal logics, although they are important for the verification of a large class of systems. This paper also discusses some of the pragmatics in verifying systems with DSYNC; and considers some extensions to the formalism. DSYNC is based on hte Hoare logic and the UNITY formalism. 

scholarly journals REASONING ABOUT TRANSFINITE SEQUENCES

2007 ◽  
Vol 18 (01) ◽  
pp. 87-112 ◽  
Author(s):  
STÉPHANE DEMRI ◽  
DAVID NOWAK
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Linear Time ◽  
Temporal Logics ◽  
Future Time ◽  
New Class ◽  
Linear Time Temporal Logic ◽  
Do So ◽  
Time Operators

We introduce a family of temporal logics to specify the behavior of systems with Zeno behaviors. We extend linear-time temporal logic LTL to authorize models admitting Zeno sequences of actions and quantitative temporal operators indexed by ordinals replace the standard next-time and until future-time operators. Our aim is to control such systems by designing controllers that safely work on ω-sequences but interact synchronously with the system in order to restrict their behaviors. We show that the satisfiability and model-checking for the logics working on ωk-sequences is EXPSPACE-complete when the integers are represented in binary, and PSPACE-complete with a unary representation. To do so, we substantially extend standard results about LTL by introducing a new class of succinct ordinal automata that can encode the interaction between the different quantitative temporal operators.

A Theory of Distributed Markov Chains

2020 ◽  
Author(s):  
P.S. Thiagarajan ◽  
Shaofa Yang
Keyword(s):  
Markov Chains ◽  
Petri Net ◽  
Linear Time ◽  
Transition System ◽  
Bounded Linear ◽  
Core Theory ◽  
Disjoint Sets ◽  
Linear Time Temporal Logic ◽  
Dynamical Properties ◽  
Checking Procedure

We present the theory of distributed Markov chains (DMCs). A DMC consists of a collection of communicating probabilistic agents in which the synchronizations determine the probability distribution for the next moves of the participating agents. The key feature of a DMC is that the synchronizations are deterministic, in the sense that any two simultaneously enabled synchronizations involve disjoint sets of agents. Using our theory of DMCs we show how one can analyze the behavior using the interleaved semantics of the model. A key point is, the transition system which defines the interleaved semantics is—except in degenerate cases—not a Markov chain. Hence one must develop new techniques to analyze these behaviors exhibiting both concurrency and stochasticity. After establishing the core theory we develop a statistical model checking procedure which verifies the dynamical properties of the trajectories generated by the the model. The specifications consist of Boolean combinations of component-wise bounded linear time temporal logic formulas. We also provide a probabilistic Petri net representation of DMCs and use it to derive a probabilistic event structure semantics.

Verifying linear time temporal logic properties of concurrent Ada programs with quasar

2004 ◽  
Vol XXIV (1) ◽  
pp. 17-24 ◽  
Author(s):  
S. Evangelista ◽  
C. Kaiser ◽  
J. F. Pradat-Peyre ◽  
P. Rousseau
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Linear Time Temporal Logic

Vehicle route-sequence planning using temporal logic

2002 ◽  
Vol 16 (1) ◽  
pp. 31-38
Author(s):  
KIAM TIAN SEOW ◽  
MICHEL PASQUIER
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Simple Procedure ◽  
Precedence Constraints ◽  
Sequence Planning ◽  
Vehicle Route ◽  
Passenger Travel ◽  
State Formula ◽  
Linear Time Temporal Logic ◽  
Service Task

This paper proposes a new logical framework for vehicle route-sequence planning of passenger travel requests. Each request is a fetch-and-send service task associated with two request-locations, namely, a source and a destination. The proposed framework is developed using propositional linear time temporal logic of Manna and Pnueli. The novelty lies in the use of the formal language for both the specification and theorem-proving analysis of precedence constraints among the location visits that are inherent in route sequences. In the framework, legal route sequences—each of which visits every request location once and only once in the precedence order of fetch-and-send associated with every such request—is formalized and justified, forming a basis upon which the link between a basic precedence constraint and the corresponding canonical forbidden-state formula is formally established. Over a given base route plan, a simple procedure to generate a feasible subplan based on a specification of the forbidden-state canonical form is also given. An example demonstrates how temporal logic analysis and the proposed procedure can be applied to select a final (feasible) subplan based on additional precedence constraints.

Ein Ansatz zur formalen Verifikation von Schaltungsbeschreibungen in SystemC (An Approach for Formal Verification of Circuits in SystemC)

2003 ◽  
Vol 45 (4) ◽  
Author(s):  
Daniel Große ◽  
Rolf Drechsler
Keyword(s):  
Formal Verification ◽  
Temporal Logic ◽  
Linear Time ◽  
Linear Time Temporal Logic

ZusammenfassungDer vorgestellte Ansatz ermöglicht es, für SystemC-Schaltkreisbeschreibungen, die über einer gegebenen Gatterbibliothek definiert sind, Eigenschaften zu beweisen (engl. property checking). Als Spezifikationssprache wird LTL (linear time temporal logic) verwendet. Für den Beweis einer LTL-Eigenschaft kann die Erfüllbarkeit einer Booleschen Funktion betrachtet werden, die aus der Eigenschaft und der Schaltkreisbeschreibung mittels symbolischer Methoden konstruiert wird. Im Gegensatz zu simulationsbasierten Ansätzen kann dabei Vollständigkeit gewährleistet werden. Anhand einer Fallstudie eines skalierbaren Arbiters wird die Effizienz des Beweisverfahrens untersucht.

scholarly journals Verifying Fault-Tolerance in Probabilistic Swarm Systems

2020 ◽  
Author(s):  
Alessio Lomuscio ◽  
Edoardo Pirovano
Keyword(s):  
Fault Tolerance ◽  
Temporal Logic ◽  
Decision Problem ◽  
Swarm Robotics ◽  
Linear Time ◽  
Experimental Results ◽  
Robotic Swarms ◽  
Linear Time Temporal Logic ◽  
Probabilistic Nature

We present a method for reasoning about fault-tolerance in unbounded robotic swarms. We introduce a novel semantics that accounts for the probabilistic nature of both the swarm and possible malfunctions, as well as the unbounded nature of swarm systems. We define and interpret a variant of probabilistic linear-time temporal logic on the resulting executions, including those arising from faulty behaviour by some of the agents in the swarm. We specify the decision problem of parameterised fault-tolerance, which concerns determining whether a probabilistic specification holds under possibly faulty behaviour. We outline a verification procedure that we implement and use to study a foraging protocol from swarm robotics, and report the experimental results obtained.

scholarly journals Dynamic Linear Time Temporal Logic

1997 ◽  
Vol 4 (8) ◽  
Author(s):  
Jesper G. Henriksen ◽  
P. S. Thiagarajan
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Dynamic Logic ◽  
Order Theory ◽  
Simple Extension ◽  
Propositional Dynamic Logic ◽  
First Order ◽  
Time Semantics ◽  
Linear Time Temporal Logic ◽  
Obvious Manner

A simple extension of the propositional temporal logic of linear<br />time is proposed. The extension consists of strengthening the until<br />operator by indexing it with the regular programs of propositional<br />dynamic logic (PDL). It is shown that DLTL, the resulting logic, is<br />expressively equivalent to S1S, the monadic second-order theory<br />of omega-sequences. In fact a sublogic of DLTL which corresponds<br />to propositional dynamic logic with a linear time semantics is<br />already as expressive as S1S. We pin down in an obvious manner<br />the sublogic of DLTL which correponds to the first order fragment<br />of S1S. We show that DLTL has an exponential time decision<br />procedure. We also obtain an axiomatization of DLTL. Finally,<br />we point to some natural extensions of the approach presented<br />here for bringing together propositional dynamic and temporal<br />logics in a linear time setting.

Sign in / Sign up

Export Citation Format

Share Document