Abstract
We define three linear semantics for probabilistic processes based on their interaction with three types of environments: trace, broom and barbed. These semantics are formalized using three recursive logics. Formulas in the logics have a maximal and a minimal interpretation. The maximal interpretation can be used to express safety properties, while the minimal interpretation can be used to express liveness properties. We present a local model checker for subsets of the logics based on a tableau system.
This work was partially supported by the Swedish National Board for Industrial and Technical Development (NUTEK).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
J.A. Bergstra and J.W. Klop. Process algebra for synchronous communication. Information and Control, 60:109–137, 1984.
L. Christoff and I. Christoff. Efficient algorithms for verification of equivalences for probabilistic processes. In Proc. 3 rd Intl. Workshop on Computer Aided Verification, LNCS 575, 310–321. Springer-Verlag, 1992.
L. Christoff and I. Christoff. Reasoning about safety and liveness properties for probabilistic processes. Technical Report DoCS 92/34, Department of Computer Systems, Uppsala University, Uppsala, Sweden, 1992.
E. Clarke and A. Emerson. Design and synthesis of synchronization skeletons using branching time Temporal Logic. In Proc. Workshop on Logics of Programs, LNCS 131, 52–71. Springer-Verlag, 1982.
I. Christoff. Testing equivalences and fully abstract models for probabilistic processes. In Proc. CONCUR '90 Theories of Concurrency: Unification and Extension, LNCS 458, 126–140. Springer-Verlag, 1990.
R. Cleaveland, S. Smolka, and A. Zwarico. Testing preorders for probabilistic processes. In Proc. 19 th Intl. Coll. on Automata, Languages and Programming, LNCS 623, 708–719. Springer-Verlag, 1992.
A. Giacalone, C.-C. Jou, and S. Smolka. Algebraic reasoning for probabilistic concurrent systems. In Proc. IFIP Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, April 1990.
R. van Glabbeek, S. Smolka, B. Steffen, and C. Tofts. Reactive, generative, and stratified models of probabilistic processes. In Proc. 5 th IEEE Symp. on Logic in Computer Science, 130–141, 1990.
H. Hansson and B. Jonsson. A framework for reasoning about time and reliability. In Proc. 10 th IEEE Real-Time Systems Symp., 1989.
H. Hansson and B. Jonsson. A calculus for communicating systems with time and probabilities. In Proc. 11 th IEEE Real-Time Systems Symp., 1990.
M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137–161, 1985.
C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
S. Hart and M. Sharir. Probabilistic Temporal Logics for finite and bounded models. In Proc. 16th ACM Symp. on Theory of Computing, 1–13, 1984.
D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333–354, 1983.
K.G. Larsen. Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theoretical Computer Science, 72:265–288, 1990.
K.G. Larsen and A. Skou. Bisimulation through probabilistic testing. In Proc. 16 th ACM Symp. on Principles of Programming Languages, 344–352, 1989.
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
A. Pnueli. Linear and branching structures in the semantics and logics of reactive systems. In Proc. 12 th Intl. Coll. on Automata, Languages and Programming, LNCS 194, 15–32. Springer-Verlag, 1985.
C. Stirling and D. Walker. Local model checking in the modal mu-calculus. In Proc. Intl. Joint Conf. on Theory and Practice of Software Development, LNCS 351, 369–383. Springer-Verlag, 1989.
A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285–309, 1955.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Christoff, L., Christoff, I. (1992). Reasoning about safety and liveness properties for probabilistic processes. In: Shyamasundar, R. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1992. Lecture Notes in Computer Science, vol 652. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56287-7_117
Download citation
DOI: https://doi.org/10.1007/3-540-56287-7_117
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56287-0
Online ISBN: 978-3-540-47507-1
eBook Packages: Springer Book Archive