Abstract
In this paper an abstract model of parallel timer processes (PTPs), allowing specification of temporal quantitative constraints on the behaviour of real time systems, is introduced. The parallel timer processes are defined in a dense time domain and are able to model both concurrent (with delay intervals overlapping on the time axis) and infinite behaviour. Both the strong and weak (abstracted from internal actions) bisimulation equivalence problems for PTPs are proved decidable. It is proved also that, if one provides the PTP model additionally with memory cells for moving timer value information along the time axis, the bisimulation equivalence (and even the vertex reachability) problems become undecidable.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur and D. Dill, Automata for Modelling Real-Time Systems, LNCS No. 443, 1990.
R. Alur, C. Courcoubetis and D. Dili, Model-Checking for Real-Time Systems, Proceedings from LICS'90 pp. 414–425, 1990.
A. Auziņš, J. Bārzdiņš, J. Bičevskis, K. Čerāns and A. Kalniņš, Automatic Construction of Test Sets: Theoretical Approach, Baltic Computer Science, LNCS, No. 502, 1991.
B. Berthomieu and M.Menasche, An Enumerative Approach for Analyzing Time Petri Nets, Proc. IFIP Congress, 1983, North-Holland, 1983.
CCITT Specification and Description Language (SDL), Recomendations Z.100, 1988.
K. Čerāns, Decidability of Bisimulation Equivalence for Parallel Timed Processes, in Proc. of Chalmers Workshop on Concurrency, Göteborg, Report PMG-R63, Chalmers University of Technology, 1992.
K. Čerāns, Feasibility of Finite and Infinite Paths in Data Dependent Programs, in Proc. for LFCS'92, Russia, Tver, LNCS No. 620, 1992.
K. Čerāns, Decidability of Bisimulation Equivalences for Processes with Parallel Timers, Technical report, Institute of Mathematics and Computer Science, University of Latvia, Riga, 1992.
K. Čerāns, Algorithmic Problems in Analysis of Real Time System Specifications, Dr.Sc.comp theses, University of Latvia, Riga, 1992.
L. Chen, Decidability and Completeness in Real Time Processes, LFCS, Edinburgh University, 1991.
C.Ghezzi, D.Mandrioli, S.Morasca and M.Pezze A General Way To Put Time in Petri Nets, ACM SIGSOFT Eng. Notes, Vol. 14, No. 3, 1989.
U. Holmer, K.Larsen and Yi Wang, Deciding Properties for Regular Real Timed Processes, CAV'91, 1991.
K.G.Larsen, Efficient Local Correctness Checking, this Workshop, 1992.
P. Merlin and D.J. Farber, Recoverability of Communication Protocols, IEEE Trans. on Communication Protocols, Vol. COM-24, No. 9, 1976.
X.Nicollin, J.Sifakis and S.Yovine, From ATP to Timed Graphs and Hybrid Systems, in Proc. of REX Workshop ”Real-Time: Theory in Practice”, 1991.
G.M. Reed and A.W. Roscoe, A Timed Model for Communicating Sequential Processes, LNCS No. 226, 1986.
Yi Wang, Real Time Behaviour of Asynchronous Agents, LNCS No. 458, 1990.
Yi Wang, CCS + Time = an Interleaving Model for Real Time Systems, ICALP'91, Madrid, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Čerāns, K. (1993). Decidability of bisimulation equivalences for parallel timer processes. In: von Bochmann, G., Probst, D.K. (eds) Computer Aided Verification. CAV 1992. Lecture Notes in Computer Science, vol 663. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56496-9_24
Download citation
DOI: https://doi.org/10.1007/3-540-56496-9_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56496-6
Online ISBN: 978-3-540-47572-9
eBook Packages: Springer Book Archive