scholarly journals Adaptive Symbolic Control for Finite-State Transition Systems With Grammatical Inference

2014 ◽  
Vol 59 (2) ◽  
pp. 505-511 ◽  
Author(s):  
Jie Fu ◽  
Herbert G. Tanner ◽  
Jeffrey Heinz ◽  
Jane Chandlee
1997 ◽  
Vol 4 (13) ◽  
Author(s):  
Jørgen H. Andersen ◽  
Kim G. Larsen

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.


2000 ◽  
Vol 11 (02) ◽  
pp. 283-314
Author(s):  
R. K. SHYAMASUNDAR ◽  
S. RAMESH

Asynchronous and Synchronous languages have been in use for the specification of reactive systems. One of the main distinguishing features of these two classes lies in the way nondeterminism is used for the specification of programs. From this viewpoint, we analyze CSP (a typical asynchronous language) and ESTEREL (a synchronous language). The synchronous language Esterel is based on the notions of determinism, input nondeterminacy and parallelism whereas CSP is built on the notions of nondeterminism, concurrency and distribution. The main objectives of the study are to assess: • The role of nondeterminism in the specification of the behaviour and realization of programs: A clear distinction between local and global nondeterminism enables us to distinguish between implementational nondeterminism and environmental/input nondeterminism. The results in this direction would enable one to achieve observable determinism where the implementational choices can be hidden and thus, analyze the program behaviour with reference to the real environmental nondeterminism in the specification. This leads to a proper refinement of specifications and aids in deriving distributed implementations of finite state transition systems that are not necessarily deterministic. • The implementability of asynchronous languages through synchronous languages. The implementability of asynchronous languages in synchronous languages not only provides a realistic implementation but also provides higher level abstractions (such as multi-process interactions) for reactive specifications using features such as broadcast, interrupts, exception handling mechanisms etc.


Author(s):  
Vincenzo Manca ◽  
Giuditta Franco ◽  
Giuseppe Scollo

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.


2010 ◽  
Vol 11 (1) ◽  
pp. 65-109 ◽  
Author(s):  
FRANK RAISER ◽  
THOM FRÜHWIRTH

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