Hans Hansson
Skip Abstract Section
Abstract
Abstract
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.
- [ABC86] Ajmone Marsan, M., Balbo, G. and Conte, G.:Performance Models of Multiprocessor Systems. MIT Press, 1986.Google Scholar
- [Abr80] Abrahamson, K.:Decidability and Expressiveness of Logics of Processes. PhD thesis, Univ. of Washington, 1980.Google Scholar
- [ACD90] Alur, R., Courcoubetis, C. and Dill, D.: Model-checking for real-time systems. InProc. 5thIEEE Int. Symp. on Logic in Computer Science, pages 414–425, 1990.Google Scholar
- [ACD91] Alur, R., Courcoubetis, C. and Dill, D.: Model-checking for probabilistic real-time systems. InProc. 18thInt. Coll. on Automata Languages and Programming (ICALP), volume 510 ofLecture Notes in Computer Science, pages 115–126. Springer Verlag, 1991.Google Scholar
- [ACD92] 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.Google Scholar
- [AlD90] Alur, R. and Dill, D.: Automata for modeling real-time systems. InProc. 17thInt. Coll. on Automata Languages and Programming (ICALP), volume 443 ofLecture Notes in Computer Science, Springer Verlag, 1990.Google Scholar
- [AlH89] Alur, R. and Henzinger, T.: A really temporal logic. InProc. 30thIEEE Annual Symp. Foundations of Computer Science, pages 164–169, 1989.Google Scholar
- [AlH92] 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.Google Scholar
- [AHU74] Aho, A.V., Hopcroft, J.E. and Ullman, J.D.:The Design and Analysis of Computer Algorithms. Addison-Wesley Publishing Company, 1974.Google Scholar
- [BeH81] Bernstein, A. and Harter, P.K.: Proving real-time properties of programs with temporal logic. InProc. 8thACM Symp. on Operating System Principles, pages 1–11, Pacific Grove, California, 1981.Google Scholar
- [BSW69] A note on reliable full-duplex transmissions over half duplex linesCommunications of the ACM196925260261Google ScholarDigital Library
- [ChC92b] Christoff, L. and Christoff, I: Reasoning about safety and liveness properties for probabilistic processes. In R. Shyamasundar, editor,Proc. 12thConf. on Foundations of Software Technology and Theoretical Computer Science, volume 652 ofLecture Notes in Computer Science, pages 342–355. Springer-Verlag, 1992.Google Scholar
- [CES86] Automatic verification of finite-state concurrent systems using temporal logic specificationACM Trans. on Programming Languages and Systems198682244263Google ScholarDigital Library
- [Chi85] 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.Google Scholar
- [CMT89] Spnp: Stochastic petri net package1989Kyoto, JapanIEEE Computer Society PressGoogle Scholar
- [CVW86] Courcoubetis, C., Vardi, M. and Wolper, P.: Reasoning about fair concurrent programs. InProc. 18thACM Symp. on Theory of Computing, pages 283–294, 1986.Google Scholar
- [CoY88] Courcoubetis, C. and Yannakakis, C.: The complexity of probabilistic verification. InProc. 29thIEEE Annual Symp. Foundations of Computer Science, pages 338–345, 1988.Google Scholar
- [CoY89] Courcoubetis, C. and Yannakakis, C.: The complexity of probabilistic verification. Bell labs Murry Hill, 1989.Google Scholar
- [dBH92] 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.Google Scholar
- [EmC82] Using branching time Temporal Logic to synthesize synchronization skeletonsScience of Computer Programming198223241266Google ScholarCross Ref
- [Eme92] 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.Google Scholar
- [EMS92] Quantitative temporal reasoningReal-Time Systems — The International Journal of Time-Critical Computing Systems19924331352Google ScholarDigital Library
- [Fel83] Feldman, Y.A.: A decidable propositional probabilistic dynamic logic. InProc. 15thACM Symp. on Theory of Computing, pages 298–309, Boston, 1983.Google Scholar
- [Gib85] Gibbons, A.:Algorithmic Graph Theory. Cambridge University Press, 1985.Google Scholar
- [Han91] 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.Google Scholar
- [HaJ90] A calculus for communicating systems with time and probabilities1990Orlando, Fl.IEEE Computer Society Press278287Google Scholar
- [Hoo91] Hooman, J.:Specification and Compositional Verification of Real-Time Systems, volume 558 ofLecture Notes in Computer Science. North-Holland, 1991.Google Scholar
- [HaS84] Hart, S. and Sharir, M.: Probabilistic temporal logics for finite and bounded models. InProc. 16thACM Symp. on Theory of Computing, pages 1–13, 1984.Google Scholar
- [HSP83] Termination of probabilistic concurrent programsACM Trans. on Programming Languages and Systems19835356380Google ScholarDigital Library
- [HoV86] 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.Google Scholar
- [HoV87a] Exact performance estimates for multiprocessor memory and bus interfaceIEEE Trans. on Computers1987C-367685Google ScholarDigital Library
- [HoV87b] 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.Google Scholar
- [JaM86] Safety analysis of timing properties in real-time systemsIEEE Trans. on Software Engineering1986SE-129890904Google ScholarDigital Library
- [JaM87] A graph-theoretic approach for timing analysis and its implementationIEEE Trans, on Computers1987368961975Google ScholarDigital Library
- [Jos88] Joseph, M.: editor.Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 331 ofLecture Notes in Computer Science. Springer Verlag, 1988.Google Scholar
- [KVR83] Koymans, R., Vytopil, J. and de Roever, W.P.: Real-time programming and asynchronous message passing. InProc. 2ndACM Symp. on Principles of Distributed Computing, pages 187–197, Montréal, Canada, 1983.Google Scholar
- [LeS82] Reasoning with time and chanceInformation and Control198253165198Google ScholarCross Ref
- [LeS89] Larsen, K.G. and Skou, A.: Bisimulation through probabilistic testing. InProc. 16thACM Symp. on Principles of Programming Languages, pages 344–352, 1989.Google Scholar
- [Mil89] Milner, R.:Communication and Concurrency. Prentice-Hall, 1989.Google Scholar
- [Mol82] Performance analysis using stochastic petri netsIEEE Trans. on Computers1982C-319913917Google ScholarDigital Library
- [OwL82] Proving liveness properties of concurrent programsACM Trans. on Programming Languages and Systems198243455495Google ScholarDigital Library
- [Ost89] 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.Google Scholar
- [OsW87] 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.Google Scholar
- [Par85] Fairness Properties in Process AlgebraPhD thesis1985Uppsala, SwedenUppsala UniversityGoogle Scholar
- [PnH88] 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.Google Scholar
- [Pnu82] The temporal semantics of concurrent programsTheoretical Computer Science1982134560Google ScholarCross Ref
- [PnZ86] Verification of multiprocess probabilistic protocolsDistributed Computing1986115372Google ScholarDigital Library
- [Raz84] 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.Google Scholar
- [RaP84] 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.Google Scholar
- [ShL87] Time dependent distributed systems: Proving safety, liveness and real-time propertiesDistributed Computing198726179Google ScholarDigital Library
- [SaM86] 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.Google Scholar
- [Var85] Vardi, M: Automatic verification of probabilistic concurrent finite-state programs. InProc. 26thIEEE Annual Symp. Foundations of Computer Science, pages 327–337, 1985.Google Scholar
- [VeH86] 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.Google Scholar
- [VaW86] 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.Google Scholar
- [Vyt91] Vytopil, P.: editor.Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 571 ofLecture Notes in Computer Science. Springer Verlag, 1991.Google Scholar
- [Zub85] Performance evaluation using extended timed Petri nets1985Torino ItalyIEEE Computer Society Press272278Google Scholar
Index Terms
- A logic for reasoning about time and reliability
Index terms have been assigned to the content through auto-classification.
Recommendations
Multi-valued Modal Fixed Point Logics for Model Checking
ISMVL '09: Proceedings of the 2009 39th International Symposium on Multiple-Valued LogicIn this paper, I will show how multi-valued logics are used for model checking. Model checking is an automatic technique to analyze correctness of hardware and software systems. A model checker is based on a temporal logic or a modal fixed point logic. ...
Probabilistic stit logic and its decomposition
We define an extension of stit logic that encompasses subjective probabilities representing beliefs about simultaneous choice exertion of other agents. This semantics enables us to express that an agent sees to it that a condition obtains under a ...
Reasoning about time-dependent multi-agents: foundations of theorem proving and model checking
Transactions on Compuational Collective Intelligence VIFirstly, an extension of linear-time temporal logic (LTL), called an agents-indexed linear-time temporal logic (ALTL), is introduced as a Gentzen-type sequent calculus. ALTL is intended to appropriately express reasoning about time-dependent multi-...
Comments