scholarly journals Reachability Analysis for Some Models of Infinite-State Transition Systems

2000 ◽  
pp. 183-198 ◽  
Author(s):  
Oscar H. Ibarra ◽  
Tevfik Bultan ◽  
Jianwen Su
Keyword(s):  
State Transition ◽  
Reachability Analysis ◽  
Transition Systems ◽  
Infinite State ◽  
State Transition Systems

scholarly journals Note on the Tableau Technique for Commutative Transition Systems

2001 ◽  
Vol 8 (50) ◽  
Author(s):  
Jirí Srba
Keyword(s):  
Wide Class ◽  
Process Algebra ◽  
State Transition ◽  
Transition System ◽  
General Technique ◽  
Transition Systems ◽  
Infinite State ◽  
State Transition Systems

We define a class of transition systems called effective commutative transition systems (ECTS) and show, by generalising a tableau-based proof for BPP, that bisimilarity between any two states of such a transition system is decidable. It gives a general technique for extending decidability borders of strong bisimilarity for a wide class of infinite-state transition systems. This is demonstrated for several process formalisms, namely BPP process algebra, lossy BPP processes, BPP systems with interrupt and timed-arc BPP nets.

scholarly journals Compositional Safety Logics

1997 ◽  
Vol 4 (13) ◽  
Author(s):  
Jørgen H. Andersen ◽  
Kim G. Larsen
Keyword(s):  
Model Checking ◽  
State Transition ◽  
Parallel Program ◽  
Transition Systems ◽  
Compositional Technique ◽  
Finite State ◽  
Necessary And Sufficient ◽  
Infinite State ◽  
State Transition Systems

In this paper we present a generalisation of a promising compositional<br /> model-checking technique introduced for finite-state systems by Andersen<br /> in [And95] and extended to networks of timed<br />automata by Larsen et al in [LPY95a, LL95, LPY95b, KLL+97a].<br />In our generalized setting, programs are modelled as arbitrary<br />(possibly infinite-state) transition systems and verified with respect<br />to properties of a basic safety logic. As the fundamental<br />prerequisite of the compositional technique, it is shown how logical<br />properties of a parallel program may be transformed into<br />necessary and sufficient properties of components of the program.<br />Finally, a set of axiomatic laws are provided useful for<br />simplifying formulae and complete with respect to validity and<br />unsatisfiability.

scholarly journals Reachability Modulo Theory Library

10.29007/f3rp ◽  
2018 ◽  
Author(s):  
Francesco Alberti ◽  
Roberto Bruttomesso ◽  
Silvio Ghilardi ◽  
Silvio Ranise ◽  
Natasha Sharygina
Keyword(s):  
Reachability Analysis ◽  
Safety Properties ◽  
Standard Language ◽  
Transition Systems ◽  
Smt Solvers ◽  
Verification Tools ◽  
Infinite State Systems ◽  
Infinite State

Reachability analysis of infinite-state systems plays a central role in many verification tasks. In the last decade, SMT-Solvers have been exploited within many verification tools to discharge proof obligations arising from reachability analysis. Despite this, as of today there is no standard language to deal with transition systems specified in the SMT-LIB format. This paper is a first proposal for a new SMT-based verification language that is suitable for defining transition systems and safety properties.

State Transition Dynamics

2011 ◽  
pp. 32-55 ◽  
Author(s):  
Vincenzo Manca ◽  
Giuditta Franco ◽  
Giuseppe Scollo
Keyword(s):  
Dynamical Systems ◽  
State Transition ◽  
Molecular Computing ◽  
Discrete Models ◽  
Classical Dynamics ◽  
Transition Systems ◽  
Transition Dynamics ◽  
Models Of Computation ◽  
Simple Set ◽  
State Transition Systems

Classical dynamics concepts are analysed in the basic mathematical setting of state transition systems where time and space are both completely discrete and no structure is assumed on the state’s space. Interesting relationships between attractors and recurrence are identified and some features of chaos are expressed in simple, set theoretic terms. String dynamics is proposed as a unifying concept for dynamical systems arising from discrete models of computation, together with illustrative examples. The relevance of state transition systems and string dynamics is discussed from the perspective of molecular computing.

Analysing graph transformation systems through constraint handling rules

2010 ◽  
Vol 11 (1) ◽  
pp. 65-109 ◽  
Author(s):  
FRANK RAISER ◽  
THOM FRÜHWIRTH
Keyword(s):  
State Transition ◽  
Graph Transformation ◽  
Constraint Handling ◽  
Transition Systems ◽  
Rule Based ◽  
Program Equivalence ◽  
Transformation Systems ◽  
Graph Transformation Systems ◽  
State Transition Systems

AbstractGraph transformation systems (GTS) and constraint handling rules (CHR) are non-deterministic rule-based state transition systems. CHR is well known for its powerful confluence and program equivalence analyses, for which we provide the basis in this work to apply them to GTS. We give a sound and complete embedding of GTS in CHR, investigate confluence of an embedded GTS and provide a program equivalence analysis for GTS via the embedding. The results confirm the suitability of CHR-based program analyses for other formalisms embedded in CHR.

Sign in / Sign up

Export Citation Format

Share Document