Abstract
We propose a model independent procedure for verifying properties of discrete event systems. The dynamics of such systems can be very complex, making them hard to analyze, so we resort to methods based on Monte Carlo simulation and statistical hypothesis testing. The verification is probabilistic in two senses. First, the properties, expressed as CSL formulas, can be probabilistic. Second, the result of the verification is probabilistic, and the probability of error is bounded by two parameters passed to the verification procedure. The verification of properties can be carried out in an anytime manner by starting off with loose error bounds, and gradually tightening these bounds.
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
Rajeev Alur, Costas Courcoubetis, and David Dill. Model-checking for real-time systems. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 414–425, Philadelphia, PA, June 1990. IEEE Computer Society Press.
Rajeev Alur, Costas Courcoubetis, and David Dill. Model-checking for probabilistic real-time systems. In Leach Albert, B. Monien, and M. Rodríguez Artalejo editors, Proceedings of the 18th International Colloquium on Automata, Languages and Programming, volume 510 of Lecture Notes in Computer Science, pages 115–126, Madrid, Spain, July 1991. Springer.
Adnan Aziz, Kumud Sanwal, Vigyan Singhal, and Robert Brayton. Verifying continuous time Markov chains. In Rajeev Alur and Thomas A. Henzinger, editors, Proceedings of the 8th International Conference on Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 269–276, New Brunswick, NJ, July/August 1996. Springer.
Adnan Aziz, Kumud Sanwal, Vigyan Singhal, and Robert Brayton. Model-checking continuous-time Markov chains. ACM Transactions on Computational Logic, 1(1):162–170, July 2000.
Christel Baier, Joost-Pieter Katoen, and Holger Hermanns. Approximate symbolic model checking of continuous-time Markov chains. In Jos C. M. Baeten and Sjouke Mauw, editors, Proceedings of the 10th International Conference on Concurrency Theory, volume 1664 of Lecture Notes in Computer Science, pages 146–161, Eindhoven, the Netherlands, August 1999. Springer.
James R. Bitner and Edward M. Reingold. Backtrack programming techniques. Communications of the ACM, 18(11):651–656, November 1975.
E. M. Clarke, E. Allen Emerson, and A. Prasad Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, April 1986.
Peter W. Glynn. A GSMP formalism for discrete event systems. Proceedings of the IEEE, 77(1):14–23, January 1989.
Peter W. Glynn and Donald L. Iglehart. Simulation methods for queues: An overview. Queueing Systems, 3:221–255, 1988.
Hans Hansson and Bengt Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512–535, 1994.
Ronald A. Howard. Dynamic Probabilistic Systems, volume II. John Wiley & Sons, New York, NY, 1971.
Gabriel G. Infante López, Holger Hermanns, and Joost-Pieter Katoen. Beyond memoryless distributions: Model checking semi-Markov chains. In Luca de Alfaro and Stephen Gilmore, editors, Proceedings of the 1st Joint International PAPM-PROBMIV Workshop, volume 2165 of Lecture Notes in Computer Science, pages 57–70, Aachen, Germany, September 2001. Springer.
Marta Kwiatkowska, Gethin Norman, Roberto Segala, and Jeremy Sproston. Verifying quantitative properties of continuous probabilistic timed automata. In Catuscia Palamidessi, editor, Proceedings of the 11th International Conference on Concurrency Theory, volume 1877 of Lecture Notes in Computer Science, pages 123–137, State College, PA, August 2000. Springer.
Klaus Matthes. Zur Theorie der Bedienungsprozesse. In Jaroslav Kožešník, editor, Transactions of the Third Prague Conference on Information Theory, Statistical Decision Functions, Random Processes, pages 513–528, Liblice, Czechoslovakia, June 1962. Publishing House of the Czechoslovak Academy of Sciences.
Gerald S. Shedler. Regenerative Stochastic Simulation. Academic Press, Boston, MA, 1993.
Abraham Wald. Sequential tests of statistical hypotheses. Annals of Mathematical Statistics, 16(2):117–186, June 1945.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Younes, H.L.S., Simmons, R.G. (2002). Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling. In: Brinksma, E., Larsen, K.G. (eds) Computer Aided Verification. CAV 2002. Lecture Notes in Computer Science, vol 2404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45657-0_17
Download citation
DOI: https://doi.org/10.1007/3-540-45657-0_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43997-4
Online ISBN: 978-3-540-45657-5
eBook Packages: Springer Book Archive