A logic for reasoning about time and reliability
Open accessAbstract
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.
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Integrity signals
Registry
Cites
Statistics
Claims the paper makes
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
Safety specifications could be expressed in terms of probabilistic computation tree logic (PCTL), or in terms of conjunction of linear inequalities of reachability probabilities.
“Safety specifications could be expressed in terms of probabilistic computation tree logic (PCTL) (Hansson & Jonsson, 1994), or in terms of conjunction of linear inequalities of reachability probabilities, for example.”
From Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems (2024) · cites this paper as Hansson & Jonsson, 1994
Self-check
Percentages, sums and reported differences re-computed from the paper’s own numbers.
The self-check needs the paper’s full text.
Cites
The Design and Analysis of Computer Algorithms
Aho, A. V., & Hopcroft, J. E. (1974) · CERN Document Server (European Organization for Nuclear Research) · Cited by 9,403 · see citing works
Milner, R. (1989) · Cited by 6,850 · see citing works
Automatic verification of finite-state concurrent systems using temporal logic specifications
Clarke, E. M., Emerson, E. A., & Sistla, A. P. (1986) · ACM Transactions on Programming Languages and Systems · doi:10.1145/5397.5399 · Cited by 3,570 · see citing works
An Automata-Theoretic Approach to Automatic Program Verification
Vardi, M. Y., & Wolper, P. (1986) · ORBi (University of Liège) · Cited by 1,261 · see citing works
Bisimulation through probabilistic testing
Larsen, K. G., & Skou, A. (1991) · Information and Computation · doi:10.1016/0890-5401(91)90030-6 · Cited by 1,206 · see citing works
Performance Analysis Using Stochastic Petri Nets
Molloy (1982) · IEEE Transactions on Computers · doi:10.1109/tc.1982.1676110 · Cited by 1,065 · see citing works
Automata for modeling real-time systems
Rajeev Alur, A., & Dill, D. L. (2005) · Springer eBooks · doi:10.1007/bfb0032042 · Cited by 905 · see citing works
Model-checking for real-time systems
Rajeev Alur, A., Courcoubetis, C., & Dill, D. L. (2002) · ACM/IEEE Symposium on Logic in Computer Science (LICS) · doi:10.1109/lics.1990.113766 · Cited by 899 · see citing works
Gibbons, A. (1985) · Cited by 828 · see citing works
The temporal semantics of concurrent programs
Pnueli, A. (1981) · Theoretical Computer Science · doi:10.1016/0304-3975(81)90110-9 · Cited by 697 · see citing works
Automatic verification of probabilistic concurrent finite state programs
Vardi, M. Y. (1985) · Annual Symposium on Foundations of Computer Science · doi:10.1109/sfcs.1985.12 · Cited by 683 · see citing works
Using branching time temporal logic to synthesize synchronization skeletons
Emerson, E. A., & Clarke, E. M. (1982) · Science of Computer Programming · doi:10.1016/0167-6423(83)90017-5 · Cited by 656 · see citing works
Safety analysis of timing properties in real-time systems
Jahanian, F., & Mok, A. K. (1986) · IEEE Transactions on Software Engineering · doi:10.1109/tse.1986.6313045 · Cited by 631 · see citing works
Proving Liveness Properties of Concurrent Programs
Owicki, S. S., & Lamport, L. (1982) · ACM Transactions on Programming Languages and Systems · doi:10.1145/357172.357178 · Cited by 576 · see citing works
Logics and models of real time: A survey
Rajeev Alur, A., & Henzinger, T. A. (1992) · Lecture notes in computer science · doi:10.1007/bfb0031988 · Cited by 556 · see citing works
SPNP: stochastic Petri net package
Ciardo, G., Muppala, J. K., & Trivedi, K. S. (2003) · International Workshop on Petri Nets and Performance Models · doi:10.1109/pnpm.1989.68548 · Cited by 547 · see citing works
A note on reliable full-duplex transmission over half-duplex links
Bartlett, K. A., Scantlebury, R. A., & Wilkinson, P. T. (1969) · Communications of the ACM · doi:10.1145/362946.362970 · Cited by 443 · see citing works
de Bakker, J. W., Huizing, C., de Roever, W. P., & Rozenberg, G. (1992) · Lecture notes in computer science · doi:10.1007/bfb0031984 · Cited by 355 · see citing works
A Generalized Timed Petri Net Model for Performance Analysis
Holliday, M. A., & Vernon, M. K. (1987) · IEEE Transactions on Software Engineering · doi:10.1109/tse.1987.233141 · Cited by 277 · see citing works
Performance models of multiprocessor systems
Marsan, M. A., Conte, G., & BALBO, G. (1987) · Microprocessors and Microsystems · doi:10.1016/0141-9331(87)90305-x · Cited by 263 · see citing works
A calculus for communicating systems with time and probabilities
Hansson, H., & Jönsson, B. (1990) · IEEE Real-Time Systems Symposium (RTSS) · doi:10.1109/real.1990.128759 · Cited by 198 · see citing works
Self-citationModel-checking for probabilistic real-time systems
Rajeev Alur, A., Courcoubetis, C., & Dill, D. L. (1991) · Lecture notes in computer science · doi:10.1007/3-540-54233-7_128 · Cited by 179 · see citing works
Termination of Probabilistic Concurrent Program
Sergiu Hart, A., Sharir, M., & Pnueli, A. (1983) · ACM Transactions on Programming Languages and Systems · doi:10.1145/2166.357214 · Cited by 164 · see citing works
Rajeev Alur, A., & Henzinger, T. A. (1989) · Annual Symposium on Foundations of Computer Science · doi:10.1109/sfcs.1989.63473 · Cited by 162 · see citing works
Quantitative temporal reasoning
Emerson, E. A., Mok, A. K., Sistla, A. P., & Srinivasan, J. (1992) · Real-Time Systems · doi:10.1007/bf00355298 · Cited by 161 · see citing works
Bisimulation through probabilistic testing (preliminary report)
Larsen, K. G., & Skou, A. (1989) · ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) · doi:10.1145/75277.75307 · Cited by 150 · see citing works
A Graph-Theoretic Approach for Timing Analysis and its Implementation
Jahanian, F., & Mok, A. K. (1987) · IEEE Transactions on Computers · doi:10.1109/tc.1987.5009519 · Cited by 149 · see citing works
Specification and Compositional Verification of Real-Time Systems
Hooman, J. (1991) · Lecture notes in computer science · doi:10.1007/3-540-54947-1 · Cited by 144 · see citing works
Reasoning with time and chance
Lehmann, D. J., & Shelah, S. (1982) · Information and Control · doi:10.1016/s0019-9958(82)91022-1 · Cited by 136 · see citing works
Verifying temporal properties of finite-state probabilistic programs
Courcoubetis, C., & Yannakakis, M. (1988) · Annual Symposium on Foundations of Computer Science · doi:10.1109/sfcs.1988.21950 · Cited by 126 · see citing works
Verification of multiprocess probabilistic protocols
Pnueli, A., & Zuck, L. D. (1986) · Distributed Computing · doi:10.1007/bf01843570 · Cited by 123 · see citing works
Real-time programming and asynchronous message passing
Koymans, R., Vytopil, J., & de Roever, W. P. (1983) · ACM Symposium on Principles of Distributed Computing (PODC) · doi:10.1145/800221.806721 · Cited by 118 · see citing works
Proving real-time properties of programs with temporal logic
Bernstein, A. J., & Harter, P. K. (1981) · ACM SIGOPS Operating Systems Review · doi:10.1145/1067627.806585 · Cited by 112 · see citing works
Applications of temporal logic to the specification of real time systems
Pnueli, A., & Harel, E. (1988) · Lecture notes in computer science · doi:10.1007/3-540-50302-1_4 · Cited by 109 · see citing works
A Software Package for the Analysis of Generalized Stochastic Petri Net Models
Chiola, G. (1985) · Cited by 95 · see citing works
Probabilistic temporal logics for finite and bounded models
Sergiu Hart, A., & Sharir, M. (1984) · ACM Symposium on Theory of Computing (STOC) · doi:10.1145/800057.808660 · Cited by 78 · see citing works
Time-dependent distributed systems: proving safety, liveness and real-time properties
Shankar, A. U., & Lam, S. S. (1987) · Distributed Computing · doi:10.1007/bf01667079 · Cited by 66 · see citing works
Decidability and expressiveness of logics of processes
Abrahamson, K. (1980) · Defense Technical Information Center (DTIC) · Cited by 61 · see citing works
Verifying automata specifications of probabilistic real-time systems
Rajeev Alur, A., Courcoubetis, C., & Dill, D. L. (1992) · Lecture notes in computer science · doi:10.1007/bfb0031986 · Cited by 56 · see citing works
Exact Performance Estimates for Multiprocessor Memory and Bus Interference
Holliday, M. A., & Vernon, M. K. (1987) · IEEE Transactions on Computers · doi:10.1109/tc.1987.5009450 · Cited by 54 · see citing works
Modelling, Specifying, and Verifying Real-Time Embedded Computer Systems.
Ostroff, J. S., & Wonham, W. M. (1987) · IEEE Real-Time Systems Symposium (RTSS) · Cited by 53 · see citing works
Vernon, M. K., & Holliday, M. A. (1986) · doi:10.1145/317499.317534 · Cited by 42 · see citing works
Performance Analysis of Multiprocessor Systems
Marsan, M. A., Conte, G., & Balbo, G. (1985) · Springer eBooks · doi:10.1007/978-94-009-5408-3_2 · Cited by 40 · see citing works
Reasoning about fair concurrent programs
Courcoubetis, C., Vardi, M. Y., & Wolper, P. (1986) · ACM Symposium on Theory of Computing (STOC) · doi:10.1145/12130.12159 · Cited by 32 · see citing works
The derivation of performance expressions for communication protocols from timed petri net models
Razouk, R. R. (1984) · ACM SIGCOMM Computer Communication Review · doi:10.1145/639624.802080 · Cited by 32 · see citing works
Formal Techniques in Real-Time and Fault-Tolerant Systems
(1991) · Lecture notes in computer science · doi:10.1007/3-540-55092-5 · Cited by 26 · see citing works
Automated verification of timed transition models
Ostroff, J. S. (1990) · Lecture notes in computer science · doi:10.1007/3-540-52148-8_20 · Cited by 24 · see citing works
A decidable propositional probabilistic dynamic logic
Feidman, Y. A. (1983) · ACM Symposium on Theory of Computing (STOC) · doi:10.1145/800061.808759 · Cited by 17 · see citing works
Formal Techniques in Real-Time and Fault-Tolerant Systems
(1988) · Lecture notes in computer science · doi:10.1007/3-540-50302-1 · Cited by 17 · see citing works
The GTPN analyzer: numerical methods and user interface
Holliday, M. A., & Vernon, M. K. (1986) · Minds at UW (University of Wisconsin) · doi:10.5555/324493.325062 · Cited by 14 · see citing works
Real-time and the Mu-Calculus (preliminary report)
Emerson, E. A. (1992) · Lecture notes in computer science · doi:10.1007/bfb0031992 · Cited by 13 · see citing works
Reasoning about safety and liveness properties for probabilistic processes
Christoff, L., & Christoff, I. (1992) · Lecture notes in computer science · doi:10.1007/3-540-56287-7_117 · Cited by 11 · see citing works
The derivation of performance expressions for communication protocols from timed petri net models
Razouk, R. R. (1984) · ACM SIGCOMM Conference (SIGCOMM) · doi:10.1145/800056.802080 · Cited by 3 · see citing works
Proving real-time properties of programs with temporal logic
Bernstein, A., & Harter, P. K. (1981) · Proceedings of the eighth symposium on Operating systems principles - SOSP '81 · doi:10.1145/800216.806585
Termination of probabilistic concurrent programs: (extended abstract)
Hart, S., Sharir, M., & Pnueli, A. (1982) · Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '82 · doi:10.1145/582153.582154
Performance evaluation using unbounded timed Petri nets
Zuberek, W. M. (n.d.) · Proceedings of the Third International Workshop on Petri Nets and Performance Models, PNPM89 · doi:10.1109/pnpm.1989.68551
Flagged first, then by citations
Research works printed but not linked: 7
- Courcoubetis, C. and Yannakakis, C.: The complexity of probabilistic verification. In Proc. 29 th IEEE Annual Symp. Foundations of Computer Science, pages 338-345, 1988.
- 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 of Lecture Notes in Computer Science, pages 176-194. Springer Verlag, 1992.
- 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.
- Larsen, K.G. and Skou, A.: Bisimulation through probabilistie testing. In Proc. 16 th ACM Syrup. on Principles of Programming Languages, pages 344-352, 1989.
- Parrow, J.: Fairness Properties in Process Algebra. PhD thesis, Uppsala University, Uppsala, Sweden, t985. Available as report DoCS 85/03, Department of Computer Systems, Uppsala University, Sweden.
- Razouk, R.R. and Phelps, C.V.: Performance analysis of timed Petri net models. In Proc. IFIP WG 6.2 Symp. on Protocol Specification, Testing, and Verification IV, pages 126-129. North-Holland, June 1984.
- Sanders, W.H. and Meyer, J.E: Metasan: a performability evaluation tool based on stochastic activity networks. In Proc of the ACM-IEEE Comp. Soc. Fall Joint Conf. IEEE Computer Society Press, November 1986.
Cited by
Sorted by citations
Model-checking algorithms for continuous-time markov chains
Christel Baier, A., Haverkort, B. R. H. M., Hermanns, H., & Katoen, J.-P. (2003) · IEEE Transactions on Software Engineering · doi:10.1109/tse.2003.1205180 · Cited by 762 · see citing works
PRISM: Probabilistic Symbolic Model Checker
Kwiatkowska, M., Norman, G., & Parker, D. (2002) · Computer Performance Evaluation / TOOLS · doi:10.1007/3-540-46029-2_13 · Cited by 834 · see citing works
Kwiatkowska, M., Norman, G., & Parker, D. (2007) · Springer eBooks · doi:10.1007/978-3-540-72522-0_6 · Cited by 607 · see citing works
Probabilistic symbolic model checking with PRISM: a hybrid approach
Kwiatkowska, M., Norman, G., & Parker, D. (2004) · International Journal on Software Tools for Technology Transfer · doi:10.1007/s10009-004-0140-2 · Cited by 437 · see citing works
Model-checking continuous-time Markov chains
Aziz, A., Sanwal, K., Singhal, V., & Brayton, R. K. (2000) · ACM Transactions on Computational Logic · doi:10.1145/343369.343402 · Cited by 415 · see citing works
Model checking of probabilistic and nondeterministic systems
Bianco, A. G., & de Alfaro, L. (1995) · Lecture notes in computer science · doi:10.1007/3-540-60692-0_70 · Cited by 414 · see citing works
A Storm is Coming: A Modern Probabilistic Model Checker
Dehnert, C., Junges, S., Katoen, J.-P., & Volk, M. (2017) · Lecture notes in computer science · doi:10.1007/978-3-319-63390-9_31 · Cited by 410 · see citing works
Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling
Younes, H. L. S., & Simmons, R. G. (2002) · Lecture notes in computer science · doi:10.1007/3-540-45657-0_17 · Cited by 373 · see citing works
Gordon, A. D., Henzinger, T. A., Nori, A. V., & Rajamani, S. K. (2014) · Future of Software Engineering (FOSE) · doi:10.1145/2593882.2593900 · Cited by 372 · see citing works
Dynamic QoS Management and Optimization in Service-Based Systems
Călinescu, R., Grunske, L., Kwiatkowska, M., Mirandola, R., & Tamburrelli, G. (2010) · IEEE Transactions on Software Engineering · doi:10.1109/tse.2010.92 · Cited by 371 · see citing works
Verifying continuous time Markov chains
Aziz, A., Sanwal, K., Singhal, V., & Brayton, R. K. (1996) · Lecture notes in computer science · doi:10.1007/3-540-61474-5_75 · Cited by 347 · see citing works
Automated Verification Techniques for Probabilistic Systems
Forejt, V., Kwiatkowska, M., Norman, G., & Parker, D. (2011) · Lecture notes in computer science · doi:10.1007/978-3-642-21455-4_3 · Cited by 336 · see citing works
Automatic verification of real-time systems with discrete probability distributions
Kwiatkowska, M., Norman, G., Roberto Segala, C., & Sproston, J. (2002) · Theoretical Computer Science · doi:10.1016/s0304-3975(01)00046-9 · Cited by 333 · see citing works
Approximate Probabilistic Model Checking
Thomas Herault, A., Lassaigne, R., Magniette, F., & Sylvain Peyronnet, D. (2004) · Lecture notes in computer science · doi:10.1007/978-3-540-24622-0_8 · Cited by 300 · see citing works
A Survey of Statistical Model Checking
Agha, G., & Palmskog, K. (2018) · ACM Transactions on Modeling and Computer Simulation · doi:10.1145/3158668 · Cited by 292 · see citing works
Reasoning about partial goal satisfaction for requirements and design engineering
Letier, E., & van Lamsweerde, A. (2004) · ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) · doi:10.1145/1029894.1029905 · Cited by 265 · see citing works
The probabilistic model checker Storm
Hensel, C., Junges, S., Katoen, J.-P., Quatmann, T., & Volk, M. (2021) · International Journal on Software Tools for Technology Transfer · doi:10.1007/s10009-021-00633-z · Cited by 258 · see citing works
The ins and outs of the probabilistic model checker MRMC
Katoen, J.-P., Zapreev, I. S., Hahn, E. M., Hermanns, H., & Jansen, D. N. (2010) · Performance Evaluation · doi:10.1016/j.peva.2010.04.001 · Cited by 256 · see citing works
Kwiatkowska, M., Norman, G., & Parker, D. (2009) · ACM SIGMETRICS Performance Evaluation Review · doi:10.1145/1530873.1530882 · Cited by 250 · see citing works
On Statistical Model Checking of Stochastic Systems
Sen, K., Viswanathan, M., & Agha, G. (2005) · Lecture notes in computer science · doi:10.1007/11513988_26 · Cited by 241 · see citing works
It usually works: The temporal logic of stochastic systems
Aziz, A., Singhal, V., Balarin, F., Brayton, R. K., & Sangiovanni-Vincentelli, A. L. (1995) · Lecture notes in computer science · doi:10.1007/3-540-60045-0_48 · Cited by 224 · see citing works
Twenty years of rewriting logic
Meseguer, J. (2012) · The Journal of Logic and Algebraic Programming · doi:10.1016/j.jlap.2012.06.003 · Cited by 205 · see citing works
Performance analysis of probabilistic timed automata using digital clocks
Kwiatkowska, M., Norman, G., Parker, D., & Sproston, J. (2006) · Formal Methods in System Design · doi:10.1007/s10703-006-0005-2 · Cited by 202 · see citing works
Computational Modeling, Formal Analysis, and Tools for Systems Biology
Bartocci, E., & Lió, P. (2016) · PLoS Computational Biology · doi:10.1371/journal.pcbi.1004591 · Cited by 202 · see citing works
Statistical probabilistic model checking with a focus on time-bounded properties
Younes, H. L. S., & Simmons, R. G. (2006) · Information and Computation · doi:10.1016/j.ic.2006.05.002 · Cited by 194 · see citing works
PROBMELA: a modeling language for communicating probabilistic processes
Christel Baier, A., Ciesinski, F., & Grosser, M. (2005) · ACM/IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE) · doi:10.1109/memcod.2004.1459815 · Cited by 193 · see citing works
Symbolic and Parametric Model Checking of Discrete-Time Markov Chains
Daws, C. (2005) · Lecture notes in computer science · doi:10.1007/978-3-540-31862-0_21 · Cited by 186 · see citing works
Approximate Model Checking of Stochastic Hybrid Systems
Abate, A., Katoen, J.-P., Lygeros, J., & Prandini, M. (2010) · European Journal of Control · doi:10.3166/ejc.16.624-641 · Cited by 179 · see citing works
Probabilistic reachability for parametric Markov models
Hahn, E. M., Hermanns, H., & Zhang, L. (2010) · International Journal on Software Tools for Technology Transfer · doi:10.1007/s10009-010-0146-x · Cited by 178 · see citing works
Engineering Trustworthy Self-Adaptive Software with Dynamic Assurance Cases
Călinescu, R., Weyns, D., Gerasimou, S., Iftikhar, M. U., Habli, I., & Kelly, T. (2017) · IEEE Transactions on Software Engineering · doi:10.1109/tse.2017.2738640 · Cited by 177 · see citing works
A review of causal inference for biomedical informatics
Kleinberg, S., & Hripcsak, G. M. (2011) · Journal of Biomedical Informatics · doi:10.1016/j.jbi.2011.07.001 · Cited by 173 · see citing works
Model Checking Continuous-Time Markov Chains by Transient Analysis
Christel Baier, A., Haverkort, B. R. H. M., Hermanns, H., & Katoen, J.-P. (2000) · Lecture notes in computer science · doi:10.1007/10722167_28 · Cited by 172 · see citing works
VESTA: A statistical model-checker and analyzer for probabilistic systems
Sen, K., Viswanathan, M., & Agha, G. (2005) · International Conference on the Quantitative Evaluation of Systems (QEST) · doi:10.1109/qest.2005.42 · Cited by 169 · see citing works
Hermanns, H., Wachter, B., & Zhang, L. (2008) · Lecture notes in computer science · doi:10.1007/978-3-540-70545-1_16 · Cited by 169 · see citing works
Specification patterns for probabilistic quality properties
Grunske, L. (2008) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1145/1368088.1368094 · Cited by 165 · see citing works
The Probabilistic Model Checking Landscape
Katoen, J.-P. (2016) · ACM/IEEE Symposium on Logic in Computer Science (LICS) · doi:10.1145/2933575.2934574 · Cited by 165 · see citing works
Symbolic model checking for probabilistic processes
Christel Baier, A., Clarke, E. M., Hartonas-Garmhausen, V., Kwiatkowska, M., & Ryan, M. D. (1997) · Lecture notes in computer science · doi:10.1007/3-540-63165-8_199 · Cited by 165 · see citing works
Comparative branching-time semantics for Markov chains
Christel Baier, A., Katoen, J.-P., Hermanns, H., & Wolf, V. (2005) · Information and Computation · doi:10.1016/j.ic.2005.03.001 · Cited by 164 · see citing works
Ymer: A Statistical Model Checker
Younes, H. L. S. (2005) · Lecture notes in computer science · doi:10.1007/11513988_43 · Cited by 163 · see citing works
Verification and planning for stochastic processes with asynchronous events
Younes, H. L. S., & Simmons, R. G. (2004) · Cited by 162 · see citing works
Symbolic model checking for probabilistic timed automata
Kwiatkowska, M., Norman, G., Sproston, J., & Wang, F. (2007) · Information and Computation · doi:10.1016/j.ic.2007.01.004 · Cited by 158 · see citing works
PMaude: Rewrite-based Specification Language for Probabilistic Object Systems
Agha, G., Meseguer, J., & Sen, K. (2006) · Electronic Notes in Theoretical Computer Science · doi:10.1016/j.entcs.2005.10.040 · Cited by 158 · see citing works
Reachability Analysis of Probabilistic Systems by Successive Refinements
D’Argenio, P. R., Jeannet, B., Jensen, H. E., & Larsen, K. G. (2001) · Lecture notes in computer science · doi:10.1007/3-540-44804-7_3 · Cited by 155 · see citing works
Weak bisimulation for fully probabilistic processes
Christel Baier, A., & Hermanns, H. (1997) · Lecture notes in computer science · doi:10.1007/3-540-63166-6_14 · Cited by 151 · see citing works
Jönsson, B., Wang, Y., & Larsen, K. G. (2001) · Elsevier eBooks · doi:10.1016/b978-044482830-9/50029-1 · Cited by 150 · see citing works
Grosu, R., & Smolka, S. A. (2005) · Lecture notes in computer science · doi:10.1007/978-3-540-31980-1_18 · Cited by 148 · see citing works
Discrete-Time Rewards Model-Checked
Andova, S., Hermanns, H., & Katoen, J.-P. (2004) · Lecture notes in computer science · doi:10.1007/978-3-540-40903-8_8 · Cited by 143 · see citing works
On Probabilistic Computation Tree Logic
Ciesinski, F., & Größer, M. (2004) · Lecture notes in computer science · doi:10.1007/978-3-540-24611-4_5 · Cited by 138 · see citing works
Automatic verification of competitive stochastic systems
Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., & Šimaitis, A. (2013) · Formal Methods in System Design · doi:10.1007/s10703-013-0183-7 · Cited by 136 · see citing works
Quantitative analysis and model checking
Huth, M., & Kwiatkowska, M. (2002) · ACM/IEEE Symposium on Logic in Computer Science (LICS) · doi:10.1109/lics.1997.614940 · Cited by 135 · see citing works
Approximative Symbolic Model Checking of Continuous-Time Markov Chains
Christel Baier, A., Katoen, J.-P., & Hermanns, H. (1999) · Lecture notes in computer science · doi:10.1007/3-540-48320-9_12 · Cited by 130 · see citing works
Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol
Kwiatkowska, M., Norman, G., & Sproston, J. (2002) · Lecture notes in computer science · doi:10.1007/3-540-45605-8_11 · Cited by 129 · see citing works
Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation
de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., & Roberto Segala, C. (2000) · Lecture notes in computer science · doi:10.1007/3-540-46419-0_27 · Cited by 129 · see citing works
Computational modelling for decision-making: where, why, what, who and how
Calder, M., Craig, C., Culley, D., de Cani, R., Donnelly, C. A., Douglas, R., Edmonds, B., Gascoigne, J., Gilbert, N., Hargrove, C., et al. (2018) · Royal Society Open Science · doi:10.1098/rsos.172096 · Cited by 127 · see citing works
Criticality Analysis for the Verification and Validation of Automated Vehicles
Neurohr, C., Westhofen, L., Butz, M., Bollmann, M. H., Eberle, U., & Galbas, R. (2021) · IEEE Access · doi:10.1109/access.2021.3053159 · Cited by 127 · see citing works
Deciding Bisimilarity and Similarity for Probabilistic Processes
Christel Baier, A., Engelen, B., & Majster-Cederbaum, M. (2000) · Journal of Computer and System Sciences · doi:10.1006/jcss.1999.1683 · Cited by 127 · see citing works
Model checking probabilistic pushdown automata
Esparza, J., Kučera, A., & Mayr, R. (2004) · doi:10.1109/lics.2004.23 · Cited by 124 · see citing works
Bayesian statistical model checking with application to Simulink/Stateflow verification
Zuliani, P., Platzer, A., & Clarke, E. M. (2010) · ACM International Conference on Hybrid Systems: Computation and Control (HSCC) · doi:10.1145/1755952.1755987 · Cited by 121 · see citing works
Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking
Katoen, J.-P., Kemna, T., Zapreev, I. S., & Jansen, D. N. (2007) · Springer eBooks · doi:10.1007/978-3-540-71209-1_9 · Cited by 121 · see citing works
On the Logical Characterisation of Performability Properties
Christel Baier, A., Haverkort, B. R. H. M., Hermanns, H., & Katoen, J.-P. (2000) · Lecture notes in computer science · doi:10.1007/3-540-45022-x_65 · Cited by 120 · see citing works
Counterexample Generation in Probabilistic Model Checking
Han, T., Katoen, J.-P., & Damman, B. (2009) · IEEE Transactions on Software Engineering · doi:10.1109/tse.2009.5 · Cited by 118 · see citing works
Model checking for probability and time: from theory to practice
Kwiatkowska, M. (2003) · ACM/IEEE Symposium on Logic in Computer Science (LICS) · doi:10.1109/lics.2003.1210075 · Cited by 118 · see citing works
Supporting Self-Adaptation via Quantitative Verification and Sensitivity Analysis at Run Time
Filieri, A., Tamburrelli, G., & Ghezzi, C. (2015) · IEEE Transactions on Software Engineering · doi:10.1109/tse.2015.2421318 · Cited by 113 · see citing works
Formal Verification and Synthesis for Discrete-Time Stochastic Systems
Lahijanian, M., Andersson, S. B., & Belta, C. A. (2015) · IEEE Transactions on Automatic Control · doi:10.1109/tac.2015.2398883 · Cited by 113 · see citing works
PVeStA: A Parallel Statistical Model Checking and Quantitative Analysis Tool
Alturki, M. A., & Meseguer, J. (2011) · Lecture notes in computer science · doi:10.1007/978-3-642-22944-2_28 · Cited by 112 · see citing works
Model checking for probabilistic timed automata
Norman, G., Parker, D., & Sproston, J. (2012) · Formal Methods in System Design · doi:10.1007/s10703-012-0177-x · Cited by 111 · see citing works
Model Repair for Probabilistic Systems
Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C. R., & Smolka, S. A. (2011) · Lecture notes in computer science · doi:10.1007/978-3-642-19835-9_30 · Cited by 110 · see citing works
Bayesian statistical model checking with application to Stateflow/Simulink verification
Zuliani, P., Platzer, A., & Clarke, E. M. (2013) · Formal Methods in System Design · doi:10.1007/s10703-013-0195-3 · Cited by 110 · see citing works
Model-Checking Markov Chains in the Presence of Uncertainties
Sen, K., Viswanathan, M., & Agha, G. (2006) · Lecture notes in computer science · doi:10.1007/11691372_26 · Cited by 110 · see citing works
Verifying Probabilistic Procedural Programs
Esparza, J., & Etessami, K. (2004) · Lecture notes in computer science · doi:10.1007/978-3-540-30538-5_2 · Cited by 108 · see citing works
Machine Learning Biochemical Networks from Temporal Logic Properties
Calzone, L., Chabrier-Rivier, N., Fages, F., & Soliman, S. (2006) · Lecture notes in computer science · doi:10.1007/11880646_4 · Cited by 107 · see citing works
Model Checking Probabilistic Systems
Christel Baier, A., de Alfaro, L., Forejt, V., & Kwiatkowska, M. (2018) · Springer eBooks · doi:10.1007/978-3-319-10575-8_28 · Cited by 107 · see citing works
Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., & Siegle, M. (2000) · Lecture notes in computer science · doi:10.1007/3-540-46419-0_24 · Cited by 105 · see citing works
Probabilistic Automata: System Types, Parallel Composition and Comparison
Sokolova, A., & de Vink, E. P. (2004) · Lecture notes in computer science · doi:10.1007/978-3-540-24611-4_1 · Cited by 103 · see citing works
Specifying Performance Measures for PEPA
Clark, G., Gilmore, S. T., & Hillston, J. E. (1999) · Lecture notes in computer science · doi:10.1007/3-540-48778-6_13 · Cited by 102 · see citing works
Lahijanian, M., Wasniewski, J., Andersson, S. B., & Belta, C. A. (2010) · Proceedings - IEEE International Conference on Robotics and Automation/Proceedings · doi:10.1109/robot.2010.5509686 · Cited by 101 · see citing works
Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach
Kwiatkowska, M., Norman, G., & Parker, D. (2002) · Lecture notes in computer science · doi:10.1007/3-540-46002-0_5 · Cited by 101 · see citing works
Kwiatkowska, M., Norman, G., & Sproston, J. (2003) · Formal Aspects of Computing · doi:10.1007/s001650300007 · Cited by 99 · see citing works
Analysing robot swarm behaviour via probabilistic model checking
Konur, S., Dixon, C., & Fisher, M. (2011) · Robotics and Autonomous Systems · doi:10.1016/j.robot.2011.10.005 · Cited by 98 · see citing works
Validation of Decentralised Smart Contracts Through Game Theory and Formal Methods
Bigi, G., Bracciali, A., Meacci, G., & Tuosto, E. (2015) · Lecture notes in computer science · doi:10.1007/978-3-319-25527-9_11 · Cited by 97 · see citing works
Quantitative Analysis With the Probabilistic Model Checker PRISM
Kwiatkowska, M., Norman, G., & Parker, D. (2006) · Electronic Notes in Theoretical Computer Science · doi:10.1016/j.entcs.2005.10.030 · Cited by 96 · see citing works
Using quantitative analysis to implement autonomic IT systems
Călinescu, R., & Kwiatkowska, M. (2009) · ACM/IEEE International Conference on Software Engineering: Companion Proceedings (ICSE-Companion) · doi:10.1109/icse.2009.5070512 · Cited by 96 · see citing works
The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems
Bozzano, M., Cimatti, A., Katoen, J.-P., Nguyen, V. Y., Noll, T., & Roveri, M. (2009) · Lecture notes in computer science · doi:10.1007/978-3-642-04468-7_15 · Cited by 96 · see citing works
Don’t Know in Probabilistic Systems
Fecher, H., Leucker, M., & Wolf, V. (2006) · Lecture notes in computer science · doi:10.1007/11691617_5 · Cited by 95 · see citing works
Approximating labelled Markov processes
Desharnais, J., Gupta, V., Jagadeesan, R., & Panangaden, P. (2003) · Information and Computation · doi:10.1016/s0890-5401(03)00051-8 · Cited by 95 · see citing works
Game-based Abstraction for Markov Decision Processes
Parker, D., Norman, G., & Kwiatkowska, M. (2006) · International Conference on the Quantitative Evaluation of Systems (QEST) · doi:10.1109/qest.2006.19 · Cited by 95 · see citing works
Model checking quantum Markov chains
Feng, Y., Yu, N., & Ying, M. (2013) · Journal of Computer and System Sciences · doi:10.1016/j.jcss.2013.04.002 · Cited by 92 · see citing works
Synthesis for PCTL in Parametric Markov Decision Processes
Hahn, E. M., Han, T., & Zhang, L. (2011) · Lecture notes in computer science · doi:10.1007/978-3-642-20398-5_12 · Cited by 92 · see citing works
Verifying Quantitative Properties of Continuous Probabilistic Timed Automata
Kwiatkowska, M., Norman, G., Roberto Segala, C., & Sproston, J. (2000) · Lecture notes in computer science · doi:10.1007/3-540-44618-4_11 · Cited by 92 · see citing works
A Model Checking Approach to the Parameter Estimation of Biochemical Pathways
Donaldson, R. A., & Gilbert, D. (2008) · Lecture notes in computer science · doi:10.1007/978-3-540-88562-7_20 · Cited by 92 · see citing works
Logic and stochastic modeling with S m A r T
Ciardo, G., Jones, R. L., Miner, A. S., & Siminiceanu, R. I. (2005) · Performance Evaluation · doi:10.1016/j.peva.2005.06.001 · Cited by 91 · see citing works
Probabilistic Abstract Interpretation
Cousot, P. M., & Monerau, M. (2012) · Lecture notes in computer science · doi:10.1007/978-3-642-28869-2_9 · Cited by 91 · see citing works
Decidable Model Checking of Probabilistic Hybrid Automata
Sproston, J. (2000) · Lecture notes in computer science · doi:10.1007/3-540-45352-0_5 · Cited by 90 · see citing works
Using probabilistic model checking in systems biology
Kwiatkowska, M., Norman, G., & Parker, D. (2008) · ACM SIGMETRICS Performance Evaluation Review · doi:10.1145/1364644.1364651 · Cited by 90 · see citing works
Counterexamples in Probabilistic Model Checking
Han, T., & Katoen, J.-P. (2007) · Springer eBooks · doi:10.1007/978-3-540-71209-1_8 · Cited by 90 · see citing works
The Ins and Outs of the Probabilistic Model Checker MRMC
Katoen, J.-P., Zapree, I. S., Hahn, E. M., Hermanns, H., & Jansen, D. N. (2009) · International Conference on the Quantitative Evaluation of Systems (QEST) · doi:10.1109/qest.2009.11 · Cited by 89 · see citing works
On probabilistic timed automata
Beauquier, D. (2003) · Theoretical Computer Science · doi:10.1016/s0304-3975(01)00215-8 · Cited by 89 · see citing works
How to specify and verify the long-run average behaviour of probabilistic systems
de Alfaro, L. (2002) · ACM/IEEE Symposium on Logic in Computer Science (LICS) · doi:10.1109/lics.1998.705679 · Cited by 89 · see citing works
A tool for model-checking Markov chains
Katoen, J.-P., Meyer-Kayser, J., Siegle, M., & Hermanns, H. (2003) · International Journal on Software Tools for Technology Transfer · doi:10.1007/s100090100072 · Cited by 89 · see citing works
Kwiatkowska, M. (2007) · ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) · doi:10.1145/1287624.1287688 · Cited by 88 · see citing works
- Authors
- Hansson, H., & Jonsson, B.
- Affiliations
- Uppsala University (SE)
- Department of Computer Systems, Uppsala University, Box 325, S-751 05, Uppsala, Sweden
- ORCID
- Hansson, Hans
- Venue
- Formal Aspects of Computing
- Published
- 1994-09
- Volume
- 6
- Issue
- 5
- Pages
- 512-535
- ISSN
- 0934-5043 (ISSN-L)
- 1433-299X
- OpenAlex
- W2005998857
- Cited by
- 1,372
- References
- 55
- Citations by year
- 2026: 28 · 2025: 35 · 2024: 35 · 2023: 53 · 2022: 53 · 2021: 51 · 2020: 38 · 2019: 58 · 2018: 56 · 2017: 51 · 2016: 57 · 2015: 75 · 2014: 89 · 2013: 77 · 2012: 66
- FWCI
- 4.88
- Type
- journal article
- Language
- en
- Open access
- bronze
- doi.org
- Licence
- www.springer.com/tdm (tdm)
- Locations
- Formal Aspects of Computing (publishedVersion)
- KTH Publication Database DiVA (KTH Royal Institute of Technology) (submittedVersion, other-oa)
- Topics
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
- Physical Sciences › Computer Science › Artificial Intelligence › Logic, Reasoning, and Knowledge
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Petri Nets in System Modeling
- Keywords
- probabilistic temporal logic, cytotoxic T lymphocytes, discrete-time Markov chains, reliability, model checking, verification algorithms
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
