Publications of Jeremy Sproston


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

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

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. © 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. © 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.


Last modified: 27/07/2017