scholarly journals Unifying Equivalences for Timed Transition Systems

10.29007/kkds ◽  
2018 ◽  
Author(s):  
Irina Virbitskaite ◽  
Natalya Gribovskaya ◽  
Eike Best
Keyword(s):  
Real Time ◽  
Linear Time ◽  
Time Spectrum ◽  
Branching Time ◽  
Real Time Systems ◽  
Transition Systems ◽  
Abstract Characterization ◽  
Time Systems ◽  
Open Maps

Timed transition systems are a widely studied model for real-time systems.The intention of the paper is to show how several categorical (open maps, path-bisimilarity and coalgebraic) approaches to an abstract characterization ofbisimulation relate to each other and to the numerous suggested behavioral equivalences of linear time -- branching time spectrum, in the setting of timed transition systems.

scholarly journals Timed Bisimulation and Open Maps

1998 ◽  
Vol 5 (4) ◽  
Author(s):  
Mogens Nielsen ◽  
Thomas S. Hune
Keyword(s):  
Real Time ◽  
Alternative Proof ◽  
Real Time Systems ◽  
Transition Systems ◽  
The Past ◽  
Natural Choice ◽  
Categorical Framework ◽  
Time Systems ◽  
Finite Presentations ◽  
Open Maps

Formal models for real-time systems have been studied intensively over the past decade. Much of the theory of untimed systems has been lifted to real-time settings. One example is the notion of bisimulation applied to timed transition systems, which is studied here within the general categorical framework of open maps. We define a category of timed transition systems, and show how to characterize standard timed bisimulation in terms of spans of open maps with a natural choice of a path category. This allows us to apply general results from the theory of open maps, e.g. the existence of canonical models and characteristic logics. Also, we obtain here an alternative proof of decidability of bisimulation for finite transition systems, and illustrate the use of open maps in finite presentations of bisimulations

scholarly journals Reachability solution characterization of parametric real-time systems

2004 ◽  
Vol 328 (1-2) ◽  
pp. 187-201 ◽  
Author(s):  
Farn Wang ◽  
Hsu-Chun Yen
Keyword(s):  
Real Time ◽  
Real Time Systems ◽  
Time Systems

scholarly journals A Constraint Oriented Proof Methodology based on Modal Transition Systems

1994 ◽  
Vol 1 (47) ◽  
Author(s):  
Kim G. Larsen
Keyword(s):  
Real Time ◽  
Software Systems ◽  
Real Time Systems ◽  
Concurrent Software ◽  
Transition Systems ◽  
Verification Problem ◽  
Key Concepts ◽  
Formal Basis ◽  
Modal Transition Systems ◽  
Time Systems

In this paper, we present a constraint-oriented state-based proof methodology for concurrent software systems which exploits compositionality and abstraction for the reduction of the verification problem under investigation. Formal basis for this methodology are Modal Transition Systems allowing loose state-based specifications, which can be refined by successively adding constraints. Key concepts of our method are <em>projective views</em>, <em>separation of proof obligations</em>, <em> Skolemization</em> and <em>abstraction</em>. The method is even applicable to real time systems

Software Engineering for Real Time Systems

IEE Review ◽  
1992 ◽  
Vol 38 (3) ◽  
pp. 112
Author(s):  
Stuart Bennett
Keyword(s):  
Software Engineering ◽  
Real Time ◽  
Real Time Systems ◽  
Time Systems
Sign in / Sign up

Export Citation Format

Share Document