Book chapters
Modeling and Verification of Distributed Systems using Markov Decision Processes
(with M. Beccuti and G. Franceschinis).
In D. Bruneo and S. Distefano (editors),
Quantitative Assessments of Distributed Systems: Methodologies and Techniques.
Scrivener - Wiley, April 2015.
Practical Applications of Probabilistic Model Checking to Communication Protocols
(with M. Duflot, M. Kwiatkowska, G. Norman, D. Parker, S. Peyronnet and C. Picaronny).
In S. Gnesi and T. Margaria (editors),
Formal Methods for Industrial Critical Systems: A Survey of Applications, pp. 133-150.
IEEE Computer Society Press. March 2013.
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
Qualitative Reachability for Open Interval Markov Chains.
PeerJ Computer Science,
9:e1489, 2023.
Probabilistic Timed Automata with One Clock and Initialised
Clock-Dependent Probabilities.
Logical Methods in Computer Science,
17(4:6), 2021.
Probabilistic Timed Automata with Clock-Dependent Probabilities.
Fundamenta Informaticae,
178(1-2), pp. 101-138, 2021.
Verification and Control for Probabilistic Hybrid Automata with Finite Bisimulations.
Journal of Logical and Algebraic Methods in Programming,
103, pp. 46-61, 2019.
Model Checking for Probabilistic Timed Automata
(with G. Norman and D. Parker).
Formal Methods in System Design, 43(2), pp. 164-190, 2013.
An Extension of the Inverse Method to Probabilistic Timed Automata
(with É. André and L. Fribourg).
Formal Methods in System Design, 42(2), pp. 119-145, 2013.
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
Timed Games with Bounded Window Parity Objectives
(with J. C. A. Main and M. Randour).
In S. Bogomolov and D. Parker, editors,
Proceedings of the 20th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2022).
Lecture Notes in Computer Science 13465,
pp 165-182.
©
Springer, 2022.
Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives
(with J. C. A. Main and M. Randour).
In S. Haddad and D. Varacca, editors,
Proceedings of the 32nd International Conference on Concurrency Theory (CONCUR 2021),
Leibniz International Proceedings in Informatics (LIPIcs) 203,
Schloss Dagstuhl -- Leibniz-Zentrum für Informatik,
2021.
(arXiv version)
Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities.
In A. Gotsman and A. Sokolova, editors,
Proceedings of the 40th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2020).
Lecture Notes in Computer Science 12136,
pp 150-168.
©
Springer, 2020.
Qualitative Reachability for Open Interval Markov Chains.
In I. Potapov and P.-A. Reynier, editors,
Proceedings of the 12th International Conference on Reachability Problems (RP'18).
Lecture Notes in Computer Science 11123,
pp 146-160.
©
Springer, 2018.
Qualitative Analysis of VASS-Induced MDPs
(with P. A. Abdulla, R. Ciobanu, R. Mayr and A. Sangnier).
In B. Jacobs and C. Löding, editors,
Proceedings of the 19th International Conference on
Foundations of Software Science and Computation Structures (FoSSaCS'16)
, pp. 106-120.
Lecture Notes in Computer Science 9634.
©
Springer, 2016.
Verification and Control of Probabilistic Rectangular Hybrid Automata.
In S. Sankaranarayanan and E. Vicario, editors,
Proceedings of the 13th International Conference on
Formal Modeling and Analysis of Timed Systems (FORMATS'15), pp. 1-9.
Lecture Notes in Computer Science 9268.
©
Springer, 2015.
Solving Parity Games on Integer Vectors
(with P. A. Abdulla, R. Mayr and A. Sangnier).
In P. R. D'Argenio and H. C. Melgratti, editors,
Proceedings of the 24th International Conference on
Concurrency Theory (CONCUR'13), pp. 106-120.
Lecture Notes in Computer Science 8052.
©
Springer, 2013.
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), pp. 79-88.
© 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 6246.
©
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
Probabilistic Timed Automata with Clock-Dependent Probabilities.
In M. Hague and I. Potapov, editors,
Proceedings of the 11th International Workshop on Reachability Problems (RP'17).
Lecture Notes in Computer Science 10506,
pp 144-159.
©
Springer, 2017.
Analysis of Timed Properties Using the Jump-Diffusion Approximation
(with P. Ballarini, M. Beccuti, E. Bibbona, A. Horváth and R. Sirovich).
In A. Di Marco and P. Reinecke, editors,
Proceedings of the 14th European Performance Engineering Workshop
(EPEW'17).
Lecture Notes in Computer Science 10497,
pp 69-84.
©
Springer, 2017.
Exact and Approximate Abstraction for Classes of Stochastic Hybrid Systems.
In M Huisman and J. van de Pol, editors,
Proceedings of the 14th International Workshop on
Automated Verification of Critical Systems (AVOCS'14).
Electronic Communications of the EASST .
European Association of Software Science and Technology,
2014.
Extended version.
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 É. 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.
|