Book chapters
Practical Applications of Probabilistic Model Checking to Communication Protocols
(with M. Duflot, M. Kwiatkowska, G. Norman, D. Parker, S. Peyronnet and C. Picaronny)
In FMICS Handbook on (Industrial) Critical Systems,
© Springer, 2012.
To appear.
Verification of Real-time Probabilistic Systems
(with M. Kwiatkowska, G. Norman and D. Parker)
In Modeling and Verification of Real-time Systems, pp. 257-297,
ISTE - John Wiley & Sons, 2008.
Model Checking for Probabilistic Timed Systems
In C. Baier, B. Haverkort, H. Hermanns, J.-P. Katoen, M. Siegle and F. Vaandrager, editors,
Validation of Stochastic Systems,
Lecture Notes in Computer Science 2925,
pp. 189-229.
© Springer, 2004.
Journals
Model Checking Timed and Stochastic Properties with CSLTA
(with S. Donatelli and S. Haddad).
IEEE Transactions on Software Engineering, 35(2), pp. 224-240, 2009.
Model Checking Probabilistic Timed Automata with One or Two Clocks
(with M. Jurdzinski and F. Laroussinie).
Logical Methods in Computer Science, 4(3), 2008.
Symbolic Model Checking for Probabilistic Timed Automata
(with M. Kwiatkowska, G. Norman and F. Wang).
Information and Computation 205(7), pp. 1027-1077, 2007.
State Explosion in Almost-Sure Probabilistic Reachability
(with F. Laroussinie).
Information Processing Letters 102(6), pp. 236-241, 2007.
Backward Bisimulation in Markov Chain Model Checking
(with S. Donatelli).
IEEE Transactions on Software Engineering 32(8), pp. 531-546, 2006.
Performance Analysis of Probabilistic Timed Automata using Digital Clocks
(with M. Kwiatkowska, G. Norman and D. Parker).
Formal Methods in System Design 29, pp 33-78, 2006.
(PS.GZ)
(PDF)
Probabilistic Model Checking of Deadline Properties in the IEEE1394 FireWire Root
Contention Protocol
(with M. Kwiatkowska and G. Norman).
Formal Aspects of Computing 14(3), pp 295-318, 2003.
Automatic Verification of Real-time Systems with Discrete Probability
Distributions
(with M. Kwiatkowska, G. Norman and R. Segala).
Theoretical Computer Science 282, pp 101-150, 2002.
Conferences
Discrete-Time Verification and Control for Probabilistic Rectangular Hybrid Automata
In C. Palamidessi and A. Riska, editors,
Proceedings of the 8th International Conference on Quantitative Evaluation of Systems
(QEST'11).
© IEEE Computer Society Press, 2011.
Simulation and Bisimulation for Probabilistic Timed Automata
(with A. Troina).
In K. Chatterjee and T. Henzinger, editors,
Proceedings of the 8th International Conference on
Formal Modelling and Analysis of Timed Systems (FORMATS'10), pp. 213-227.
Lecture Notes in Computer Science.
©
Springer, 2010.
Strict Divergence for Probabilistic Timed Automata.
In M. Bravetti and G. Zavattaro, editors,
Proceedings of the 20th International Conference on
Concurrency Theory (CONCUR'09), pp. 620-636.
Lecture Notes in Computer Science 5710.
©
Springer, 2009.
Note: the above version of the paper corrects an error in Case (B) of Section 4 in the proceedings version.
Computing Expected Absorption Times for Parametric Determinate Probabilistic Timed Automata
(with N. Chamseddine, M. Duflot, L. Fribourg and C. Picaronny).
In S. Donatelli and P. Panangaden, editors,
Proceedings of the 5th International Conference on Quantitative Evaluation of Systems
(QEST'08), pp. 254-263.
© IEEE Computer Society Press, 2008.
CSLTA: an Expressive Logic for Continuous-Time Markov Chains
(with S. Donatelli and S. Haddad).
In M. Harchol-Balter, M. Kwiatkowska and M. Telek, editors,
Proceedings of the 4th International Conference on Quantitative Evaluation of Systems
(QEST'07), pp. 31-40.
© IEEE Computer Society Press, 2007.
Winner of the QEST'07 Best Paper Award.
Model Checking Probabilistic Timed Automata with One or Two Clocks
(with M. Jurdzinski and F. Laroussinie).
In O. Grumberg and M. Huth, editors,
Proceedings of the 13th International Conference on
Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07).
Lecture Notes in Computer Science 4424, pp. 170-184.
©
Springer, 2007.
From Time Petri Nets to Timed Automata: an Untimed Approach
(with D. D'Aprile, S. Donatelli and A. Sangnier).
In O. Grumberg and M. Huth, editors,
Proceedings of the 13th International Conference on
Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07).
Lecture Notes in Computer Science 4424, pp. 216-230.
©
Springer, 2007.
(PS.GZ)
(PDF)
CSL Model Checking for Generalized Stochastic Petri Nets
(with D. Cerotti, S. Donatelli and A. Horváth).
In P. D'Argenio, A. Miner and G. Rubino, editors,
Proceedings of the 3rd International Conference on Quantitative Evaluation of Systems
(QEST'06),
pp. 199-210.
© IEEE Computer Society Press, 2006.
(PS.GZ)
(PDF)
Verifying Stochastic Well-formed Nets with CSL Model-Checking Tools
(with D. Cerotti, D. D'Aprile and S. Donatelli).
In K. Goossens and L. Petrucci, editors,
Proceedings of the 6th International Conference on Application of Concurrency to System Design
(ACSD'06).
© IEEE Computer Society Press, 2006.
Model Checking Durational Probabilistic Systems
(with F. Laroussinie).
In V. Sassone, editor,
Proceedings of the 8th International Conference on
Foundations of Software Science and Computation Structures (FOSSACS'05).
Lecture Notes in Computer Science 3441,
pp 140-154.
©
Springer, 2005.
Backward Stochastic Bisimulation in CSL Model Checking
(with S. Donatelli).
In G. Franceschinis, J.-P. Katoen and M. Woodside, editors,
Proceedings of the 1st International Conference on
Quantitative Evaluation of Systems (QEST'04),
pp 220-229.
© IEEE Computer Society Press, 2004.
Symbolic Model Checking for Probabilistic Timed Automata
(with M. Kwiatkowska, G. Norman and F. Wang).
In Y. Lakhnech and S. Yovine, editors,
Proceedings of the Joint Conference on
Formal Modelling and Analysis of Timed Systems (FORMATS'04) and
Formal Techniques in Real-Time and Fault Tolerant System (FTRTFT'04),
Lecture Notes in Computer Science 3253,
pp 293-308.
© Springer, 2004.
See also the related technical
report.
CSL Model Checking for the GreatSPN Tool
(with D. D'Aprile and S. Donatelli).
In C. Aykanat, T. Dayar, I. Korpeoglu, editors,
Proceedings of the 19th International Symposium on Computer and Information Sciences
(ISCIS'04),
Lecture Notes in Computer Science 3280,
pp 543-552.
© Springer, 2004.
Symbolic Computation of Maximal Probabilistic Reachability
(with M. Kwiatkowska and G. Norman).
In K.G.Larsen and M.Nielsen, editors,
Proceedings of the 12th International Conference on Concurrency Theory
(CONCUR'01),
Lecture Notes in Computer Science 2154,
pp 169-183.
© Springer, 2001.
See also the technical
report.
Decidable Model Checking of Probabilistic Hybrid Automata.
In M. Joseph, editor,
Proceedings of the 6th International School and Symposium on
Formal Techniques in Real-Time and Fault-Tolerant Systems
(FTRTFT'00),
Lecture Notes in Computer Science 1926,
pp 31-45.
© Springer, 2000.
Note: a corrected version of Section 4.2 of this paper appears in my PhD thesis.
Verifying Quantitative Properties of Continuous Probabilistic Timed Automata.
(with M. Kwiatkowska, G. Norman and R. Segala).
In C. Palamidessi, editor,
Proceedings of the 11th International Conference on Concurrency Theory
(CONCUR'00),
Lecture Notes in Computer Science 1877,
pp 123-137.
© Springer, 2000.
Workshops
Performability Measure Specification: Combining CSRL and MSL
(with A. Aldini and M. Bernardo).
In G. Salaün and B. Schätz, editors,
Proceedings of the 16th International Workshop on
Formal Methods for Industrial Critical Systems (FMICS'11).
Lecture Notes in Computer Science 6959,
pp 165-179..
©
Springer, 2011.
An Extension of the Inverse Method to Probabilistic Timed Automata
(with E. André and L. Fribourg).
In M. Roggenbach, editor,
Proceedings of the 9th International Workshop on
Automated Verification of Critical Systems (AVOCS'09).
Electronic Communications of the EASST 23.
European Association of Software Science and Technology,
2009.
Performance Analysis of Probabilistic Timed Automata using Digital Clocks
(with M. Kwiatkowska, G. Norman and D. Parker).
In K.G. Larsen and P. Niebert, editors, Proceedings of the 1st International Workshop on
Formal Modeling and Analysis of Timed Systems
(FORMATS 2003),
Lecture Notes in Computer Science 2791,
pp 105-120.
© Springer, 2003.
Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network
Protocol
(with M. Kwiatkowska and G. Norman).
In H. Hermanns and R. Segala, editors, Proceedings of the 2nd Joint
International Workshop on
Process Algebra and Performance Modelling and Probabilistic Methods in
Verification
(PAPM-PROBMIV 2002),
Lecture Notes in Computer Science 2399,
pp 169-187.
© Springer, 2002.
See also the
technical report .
Probabilistic Model Checking of Deadline Properties in the IEEE1394 FireWire Root
Contention Protocol
(with M. Kwiatkowska and G. Norman).
In C.Shankland, S.Maharaj and J.Romijn, editors, Proceedings of the
International Workshop on Application of Formal Methods to IEEE 1394
Standard,
published by the University of Stirling,
2001.
Verifying Soft Deadlines with Probabilistic Timed Automata
(with M. Kwiatkowska, G. Norman and R. Segala).
In Proceedings of the Workshop on Advances in Verification (WAVe 2000).
Analyzing Subclasses of Probabilistic Hybrid Automata.
In M. Kwiatkowska, editor,
Proceedings of the 2nd International Workshop on Probabilistic Methods
in Verification
(PROBMIV'99),
Technical Report CSR-99-8, School of Computer Science, University of
Birmingham.
Automatic Verification of Real-time Systems with Discrete Probability
Distributions
(with M. Kwiatkowska, G. Norman and R. Segala).
In J.-P. Katoen, editor,
Proceedings of the 5th AMAST Workshop on Real-Time and Probabilistic
Systems
(ARTS'99),
Lecture Notes in Computer Science 1601,
pp. 55-75.
© Springer, 1999.
Thesis
Model Checking for Probabilistic Timed and Hybrid
Systems.
PhD thesis.
Technical report CSR-01-04, School of Computer Science, The University of
Birmingham, 2001.
|