Kripke modelling of multiple robots with decentralized cooperation specified with temporal logic

2005 ◽  
Vol 219 (1) ◽  
pp. 15-31 ◽  
Author(s):  
S Jeyaraman ◽  
A Tsourdos ◽  
R Zbikowski ◽  
B A White
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Possible Worlds ◽  
Autonomous Robots ◽  
Mathematical Formalism ◽  
Kripke Models ◽  
Constrained Motion ◽  
Labelling Function ◽  
Free Environment ◽  
Decentralized Cooperation

Kripke models are used to formalize decentralized cooperation of a group of robots, to propose temporal logic specification of the cooperation, and to verify the correctness of the specification by checking the models. The focus is on implementing this mathematical formalism under minimalist communication and under constrained motion of the robots. Kripke models consist of, firstly, a of possible worlds (system configurations), secondly, an accessibility relation in the (transitions between the worlds), and, thirdly, a labelling function (which logical statements are true in each world). This approach represents continuous dynamics and discrete decision making of the robots in a unified way. Desirable properties of cooperation can be precisely expressed using temporal logic statements defining safety, liveness, etc. Whether a group of robots, whose behaviour is formalized with Kripke models, possesses such properties is then verified using automated model checking tools. The scenarios considered include path planning of a group of three robots moving in an obstacle-free environment, without and with communication among group members. The results show that for each scenario the mathematical formalism of Kripke models expresses the group behaviour in a transparent and tractable way. Finally, desirable properties of the decentralized cooperation, specified with temporal logic, can be verified on the Kripke models by automatic model checking software. Hence, guaranteed performance of cooperating autonomous robots can be assured in a formal, precise, and clear way.

scholarly journals Timed ATL: Forget Memory, Just Count

2019 ◽  
Vol 66 ◽  
pp. 197-223
Author(s):  
Michal Jozef Knapik ◽  
Etienne Andre ◽  
Laure Petrucci ◽  
Wojciech Jamroga ◽  
Wojciech Penczek
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Discrete Time ◽  
The Other ◽  
Simple Pattern ◽  
Perfect Recall ◽  
Other Hand ◽  
Compact Representations ◽  
Time Extension ◽  
Number Of Visits

In this paper we investigate the Timed Alternating-Time Temporal Logic (TATL), a discrete-time extension of ATL. In particular, we propose, systematize, and further study semantic variants of TATL, based on different notions of a strategy. The notions are derived from different assumptions about the agents’ memory and observational capabilities, and range from timed perfect recall to untimed memoryless plans. We also introduce a new semantics based on counting the number of visits to locations during the play. We show that all the semantics, except for the untimed memoryless one, are equivalent when punctuality constraints are not allowed in the formulae. In fact, abilities in all those notions of a strategy collapse to the “counting” semantics with only two actions allowed per location. On the other hand, this simple pattern does not extend to the full TATL. As a consequence, we establish a hierarchy of TATL semantics, based on the expressivity of the underlying strategies, and we show when some of the semantics coincide. In particular, we prove that more compact representations are possible for a reasonable subset of TATL specifications, which should improve the efficiency of model checking and strategy synthesis.

scholarly journals Model Checking Temporal Logic Formulas Using Sticker Automata

2017 ◽  
Vol 2017 ◽  
pp. 1-33 ◽  
Author(s):  
Weijun Zhu ◽  
Changwei Feng ◽  
Huanmei Wu
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Complex Problem ◽  
Finite State Automaton ◽  
Dna Molecules ◽  
Single Stranded Dna ◽  
Finite State ◽  
Input Strings ◽  
Logic Model Checking ◽  
The Given

As an important complex problem, the temporal logic model checking problem is still far from being fully resolved under the circumstance of DNA computing, especially Computation Tree Logic (CTL), Interval Temporal Logic (ITL), and Projection Temporal Logic (PTL), because there is still a lack of approaches for DNA model checking. To address this challenge, a model checking method is proposed for checking the basic formulas in the above three temporal logic types with DNA molecules. First, one-type single-stranded DNA molecules are employed to encode the Finite State Automaton (FSA) model of the given basic formula so that a sticker automaton is obtained. On the other hand, other single-stranded DNA molecules are employed to encode the given system model so that the input strings of the sticker automaton are obtained. Next, a series of biochemical reactions are conducted between the above two types of single-stranded DNA molecules. It can then be decided whether the system satisfies the formula or not. As a result, we have developed a DNA-based approach for checking all the basic formulas of CTL, ITL, and PTL. The simulated results demonstrate the effectiveness of the new method.

scholarly journals ∞-Regular temporal logic and its model checking problem

1992 ◽  
Vol 103 (2) ◽  
pp. 191-204 ◽  
Author(s):  
Kiyoharu Hamaguchi ◽  
Hiromi Hiraishi ◽  
Shuzo Yajima
Keyword(s):  
Model Checking ◽  
Temporal Logic

Interval Temporal Logic Model Checking: The Border Between Good and Bad HS Fragments

2016 ◽  
pp. 389-405 ◽  
Author(s):  
Laura Bozzelli ◽  
Alberto Molinari ◽  
Angelo Montanari ◽  
Adriano Peron ◽  
Pietro Sala
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Logic Model ◽  
Interval Temporal Logic ◽  
Logic Model Checking
Sign in / Sign up

Export Citation Format

Share Document