×

zbMATH — the first resource for mathematics

A logic for reasoning about time and reliability. (English) Zbl 0820.68113
Summary: We present a logic for stating properties such as, “after a request for service there is at least a 98% probability that the service will be carried out within 2 seconds”. The logic extends the temporal logic CTL by Emerson, Clarke and Sistla with time and probabilities. Formulas are interpreted over discrete time Markov chains. We give algorithms for checking that a given Markov chain satisfies a formula in the logic. The algorithms require a polynomial number of arithmetic operations, in size of both the formula and the Markov chain. A simple example is included to illustrate the algorithms.

MSC:
68T27 Logic in artificial intelligence
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
GTPN; SPNP
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Ajmone Marsan, M., Balbo, G. and Conte, G.:Performance Models of Multiprocessor Systems. MIT Press, 1986.
[2] Abrahamson, K.:Decidability and Expressiveness of Logics of Processes. PhD thesis, Univ. of Washington, 1980.
[3] Alur, R., Courcoubetis, C. and Dill, D.: Model-checking for real-time systems. InProc. 5 th IEEE Int. Symp. on Logic in Computer Science, pages 414-425, 1990.
[4] Alur, R., Courcoubetis, C. and Dill, D.: Model-checking for probabilistic real-time systems. InProc. 18 th Int. Coll. on Automata Languages and Programming (ICALP), volume 510 ofLecture Notes in Computer Science, pages 115-126. Springer Verlag, 1991. · Zbl 0769.68088
[5] Alur, R., Courcoubetis, C. and Dill, D.: Verifying Automata Specifications of Probabilistic Real-Time Systems. In J. de Bakker, C. Huizing, W.-P. de Roever, and G. Rozenberg, editors,Real-Time: Theory in Practice, volume 600 ofLecture Notes in Computer Science, pages 28-44. Springer Verlag, 1992.
[6] Alur, R. and Dill, D.: Automata for modeling real-time systems. InProc. 17 th Int. Coll. on Automata Languages and Programming (ICALP), volume 443 ofLecture Notes in Computer Science, Springer Verlag, 1990. · Zbl 0765.68150
[7] Alur, R. and Henzinger, T.: A really temporal logic. InProc. 30 th IEEE Annual Symp. Foundations of Computer Science, pages 164-169, 1989.
[8] Alur, R. and Henzinger, T.: Logics and Models of Real Time: A Survey. In J. de Bakker, C. Huizing, W.-P. de Roever, and G. Rozenberg, editors,Real-Time: Theory in Practice, volume 600 ofLecture Notes in Computer Science, pages 28-44. Springer Verlag, 1992.
[9] Aho, A.V., Hopcroft, J.E. and Ullman, J.D.:The Design and Analysis of Computer Algorithms. Addison-Wesley Publishing Company, 1974. · Zbl 0326.68005
[10] Bernstein, A. and Harter, P.K.: Proving real-time properties of programs with temporal logic. InProc. 8 th ACM Symp. on Operating System Principles, pages 1-11, Pacific Grove, California, 1981.
[11] Bartlett, K., Scantlebury, R. and Wilkinson, P.: A note on reliable full-duplex transmissions over half duplex lines.Communications of the ACM, 2(5):260-261, 1969. · doi:10.1145/362946.362970
[12] Christoff, L. and Christoff, I: Reasoning about safety and liveness properties for probabilistic processes. In R. Shyamasundar, editor,Proc. 12 th Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 652 ofLecture Notes in Computer Science, pages 342-355. Springer-Verlag, 1992. · Zbl 0925.03151
[13] Clarke, E.M., Emerson, E.A. and Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specification.ACM Trans. on Programming Languages and Systems, 8(2):244-263, April 1986. · Zbl 0591.68027 · doi:10.1145/5397.5399
[14] Chiola, G.: A software package for the analysis of generalized stochastic Petri net models. InProc. Int. Workshop on Time Petri Nets, pages 136-143, July 1985.
[15] Ciardo, G., Muppala, J. and Trivedi, K.S.: Spnp: Stochastic petri net package. InProc. of the third International Workshop on Petri Nets and Performance Models. IEEE Computer Society Press, Kyoto, Japan, December 1989.
[16] Courcoubetis, C., Vardi, M. and Wolper, P.: Reasoning about fair concurrent programs. InProc. 18 th ACM Symp. on Theory of Computing, pages 283-294, 1986.
[17] Courcoubetis, C. and Yannakakis, C.: The complexity of probabilistic verification. InProc. 29 th IEEE Annual Symp. Foundations of Computer Science, pages 338-345, 1988.
[18] Courcoubetis, C. and Yannakakis, C.: The complexity of probabilistic verification. Bell labs Murry Hill, 1989. · Zbl 0885.68109
[19] de Bakker, J., Huizing, C., de Roever, W-.P. and Rozenberg, G.: editors.Real-Time: Theory in Practice, volume 600 ofLecture Notes in Computer Science. Springer Verlag, 1992.
[20] Emerson, E.A. and Clarke, E.M.: Using branching time Temporal Logic to synthesize synchronization skeletons.Science of Computer Programming, 2(3):241-266, 1982. · Zbl 0514.68032 · doi:10.1016/0167-6423(83)90017-5
[21] Emerson, A.: Real-Time and the Mu-Calculus. In J. de Bakker, C. Huizing, W-.P. de Roever, and G. Rozenberg, editors,Real-Time: Theory in Practice, volume 600 ofLecture Notes in Computer Science, pages 176-194. Springer Verlag, 1992.
[22] Emerson, A., Mok, A., Sistla, A. and Srinivasan, J.: Quantitative temporal reasoning.Real-Time Systems ? The International Journal of Time-Critical Computing Systems, 4:331-352, 1992.
[23] Feldman, Y.A.: A decidable propositional probabilistic dynamic logic. InProc. 15 th ACM Symp. on Theory of Computing, pages 298-309, Boston, 1983.
[24] Gibbons, A.:Algorithmic Graph Theory. Cambridge University Press, 1985. · Zbl 0568.05001
[25] Hansson, H.:Time and Probabilities in Formal Design of Distributed Systems. PhD thesis, Department of Computer Systems, Uppsala University, 1991. Available as report DoCS 91/27, Department of Computer Systems, Uppsala University, Sweden, and as report 05 in SICS dissertation series, SICS, Kista, Sweden. A revised version of the thesis will appear in the Elsevier book series Real-Time Safety Critical Systems.
[26] Hansson, H. and Jonsson, B.: A calculus for communicating systems with time and probabilities. InProc. 11 th IEEE Real -Time Systems Symp., pages 278-287, Orlando, Fl., December 1990. IEEE Computer Society Press.
[27] Hooman, J.:Specification and Compositional Verification of Real-Time Systems, volume 558 ofLecture Notes in Computer Science. North-Holland, 1991.
[28] Hart, S. and Sharir, M.: Probabilistic temporal logics for finite and bounded models. InProc. 16 th ACM Symp. on Theory of Computing, pages 1-13, 1984.
[29] Hart, S., Sharir, M. and Pnueli, A.: Termination of probabilistic concurrent programs.ACM Trans. on Programming Languages and Systems, 5:356-380, 1983. · Zbl 0511.68009 · doi:10.1145/2166.357214
[30] Holliday, M.A. and Vernon, M.K.: The GTPN Analyzer: numerical methods and user interface. Technical Report 639, Dept. of Computer Science, Univ. of Wisconsin ? Madison, Apr. 1986.
[31] Holliday, M.A. and Vernon, M.K.: Exact performance estimates for multiprocessor memory and bus interface.IEEE Trans. on Computers, C-36:76-85, Jan. 1987. · doi:10.1109/TC.1987.5009450
[32] Holliday, M.A. and Vernon, M.K.: A generalized timed Petri net model for performance analysis.IEEE Trans. on Software Engineering, SE-13(12), 1987.
[33] Jahanian, F. and Mok, K.-L.: Safety analysis of timing properties in real-time systems.IEEE Trans. on Software Engineering, SE-12(9):890-904, Sept. 1986.
[34] Jahanian, F. and Mok, A.K.: A graph-theoretic approach for timing analysis and its implementation.IEEE Trans, on Computers, 36(8):961-975, August 1987. · Zbl 0618.68008 · doi:10.1109/TC.1987.5009519
[35] Joseph, M.: editor.Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 331 ofLecture Notes in Computer Science. Springer Verlag, 1988.
[36] Koymans, R., Vytopil, J. and de Roever, W.P.: Real-time programming and asynchronous message passing. InProc. 2 nd ACM Symp. on Principles of Distributed Computing, pages 187-197, Montréal, Canada, 1983.
[37] Lehmann, D. and Shelah, S.: Reasoning with time and chance.Information and Control, 53:165-198, 1982. · Zbl 0523.03016 · doi:10.1016/S0019-9958(82)91022-1
[38] Larsen, K.G. and Skou, A.: Bisimulation through probabilistic testing. InProc. 16 th ACM Symp. on Principles of Programming Languages, pages 344-352, 1989. · Zbl 0756.68035
[39] Milner, R.:Communication and Concurrency. Prentice-Hall, 1989. · Zbl 0683.68008
[40] Molloy, M.K.: Performance analysis using stochastic petri nets.IEEE Trans. on Computers, C-31(9):913-917, Sept. 1982. · Zbl 05338404 · doi:10.1109/TC.1982.1676110
[41] Owicki, S. and Lamport, L.: Proving liveness properties of concurrent programs.ACM Trans. on Programming Languages and Systems, 4(3):455-495, 1982. · Zbl 0483.68013 · doi:10.1145/357172.357178
[42] Ostroff, J.: Automatic verification of timed transition models. In Sifakis, editor,Workshop on automatic verification methods for finite state systems, volume 407 ofLecture Notes in Computer Science, pages 247-256. Springer Verlag, 1989.
[43] Ostroff, J. and Wonham, W.: Modelling, specifying and verifying real-time embedded computer systems. InProc. IEEE Real-time Systems Symp., pages 124-132, Dec. 1987.
[44] Parrow, J.:Fairness Properties in Process Algebra. PhD thesis, Uppsala University, Uppsala, Sweden, 1985. Available as report DoCS 85/03, Department of Computer Systems, Uppsala University, Sweden.
[45] Pnueli, A. and Harel, E.: Applications of temporal logic to the specification of real-time systems. In M. Joseph, editor,Proc. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 331 ofLecture Notes in Computer Science, pages 84-98. Springer Verlag, 1988. · Zbl 0688.68024
[46] Pnueli, A.: The temporal semantics of concurrent programs.Theoretical Computer Science, 13:45-60, 1982. · Zbl 0441.68010 · doi:10.1016/0304-3975(81)90110-9
[47] Pnueli, A. and Zuck, L.: Verification of multiprocess probabilistic protocols.Distributed Computing, 1(1):53-72, 1986. · Zbl 0598.68019 · doi:10.1007/BF01843570
[48] Razouk, R.R.: The derivation of performance expressions for communication protocols from timed Petri net models. InProc. ACM SIGCOMM ’84, pages 210-217, Montréal, Québec, 1984.
[49] Razouk, R.R. and Phelps, C.V.: Performance analysis of timed Petri net models. InProc. IFIP WG 6.2 Symp. on Protocol Specification, Testing, and Verification IV, pages 126-129. North-Holland, June 1984.
[50] Shankar, A.U. and Lam, S.S.: Time dependent distributed systems: Proving safety, liveness and real-time properties.Distributed Computing, 2:61-79, 1987. · doi:10.1007/BF01667079
[51] Sanders, W.H. and Meyer, J.F.: Metasan: a performability evaluation tool based on stochastic activity networks. InProc of the ACM-IEEE Comp. Soc. Fall Joint Conf. IEEE Computer Society Press, November 1986.
[52] Vardi, M: Automatic verification of probabilistic concurrent finite-state programs. InProc. 26 th IEEE Annual Symp. Foundations of Computer Science, pages 327-337, 1985.
[53] Vernon, M.K. and Holliday, M.A.: Performance analysis of multiprocessor cache consistency protocols using generalized timed Petri nets. InProc. of Performance 86 and ACM SIGMETRICS 1986 Joint conf. on Computer Performance Modelling, Measurement, and Evaluation, pages 9-17. ACM press, May 1986.
[54] Vardi, M.Y. and Wolper, P.: An automata-theoretic approach to automatic program verification. InProc. IEEE Symp. on Logic in Computer Science, pages 332-344, June 1986.
[55] Vytopil, P.: editor.Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 571 ofLecture Notes in Computer Science. Springer Verlag, 1991.
[56] Zuberek, W.: Performance evaluation using extended timed Petri nets. InProc. International Workshop on Timed Petri Nets, pages 272-278, Torino Italy, 1985. IEEE Computer Society Press.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.