scholarly journals Model checking Timed CSP

10.29007/6fqk ◽  
2018 ◽  
Author(s):  
Philip Armstrong ◽  
Gavin Lowe ◽  
Joël Ouaknine ◽  
Bill Roscoe
Keyword(s):  
Model Checking ◽  
Discrete Time ◽  
Timed Csp ◽  
The Creation

Though Timed CSP was developed 25 years ago and the CSP-basedrefinement checker FDR was first released 20 years ago, there has never beena version of this tool for Timed CSP. In this paper we report on the creation ofsuch a version, based on the digitisation results of Ouaknine} andthe associated development of discrete-time versions of Timed CSP withassociated models.

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.

CHAOTIC HIERARCHY IN HIGH DIMENSIONS

2000 ◽  
Vol 14 (24) ◽  
pp. 2511-2527 ◽  
Author(s):  
D. E. POSTNOV ◽  
A. G. BALANOV ◽  
O. V. SOSNOVTSEVA ◽  
E. MOSEKILDE
Keyword(s):  
Discrete Time ◽  
Chaotic Behavior ◽  
Higher Order ◽  
Chaotic Attractors ◽  
Lyapunov Dimension ◽  
High Dimensions ◽  
Time Model ◽  
Discrete Time Model ◽  
The Creation

The paper suggests a new mechanism for the development of higher-order chaos in accordance with the concept of a chaotic hierarchy. A discrete-time model is proposed which demonstrates how the creation of coexisting chaotic attractors combined with boundary crises can produce a continued growth of the Lyapunov dimension of the resulting chaotic behavior.

scholarly journals COMPUTABLE SEMANTICS FOR CTL* ON DISCRETE-TIME AND CONTINUOUS-SPACE DYNAMIC SYSTEMS

2011 ◽  
Vol 22 (04) ◽  
pp. 801-821
Author(s):  
PIETER COLLINS ◽  
IVAN S. ZAPREEV
Keyword(s):  
Model Checking ◽  
Discrete Time ◽  
Dynamic Systems ◽  
Parallel Composition ◽  
Computable Model ◽  
Continuous Space ◽  
Büchi Automaton

In this work, we consider Discrete-Time Continuous-Space Dynamic Systems for which we study the computability of the standard semantics of CTL* (CTL, LTL) and provide a variant thereof computable in the sense of Type-2 Theory of Effectivity. In particular, we show how the computable model checking of existentially and universally quantified path formulae of LTL can be reduced to solving, respectively, repeated reachability and persistence problems on a model obtained as a parallel composition of the original one and a non-deterministic Büchi automaton corresponding to the verified LTL formula.

On the complexity of model checking interval-valued discrete time Markov chains

2013 ◽  
Vol 113 (7) ◽  
pp. 210-216 ◽  
Author(s):  
Taolue Chen ◽  
Tingting Han ◽  
Marta Kwiatkowska
Keyword(s):  
Model Checking ◽  
Markov Chains ◽  
Discrete Time ◽  
Interval Valued
Sign in / Sign up

Export Citation Format

Share Document