Gethin Norman's Publications

2022

  • M. Kwiatkowska, G. Norman, D. Parker, G. Santos and R. Yan Probabilistic Model Checking for Strategic Equilibria-based Decision Making: Advances and Challenges. In Proc. 247th International Symposium on Mathematical Foundations of Computer Science (MFCS'22), To appear. August 2022. [pdf] [bib]
  • M. Kwiatkowska, G. Norman, D. Parker and G. Santos Correlated Equilibria and Fairness in Concurrent Stochastic Games. In Proc. 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'22), volume 13244 of LNCS, pages 60–78, Springer. April 2022. [pdf] [bib] An extended version of this paper, including the complete model checking algorithm, is available at arxiv.org/abs/2201.09702
    Supporting material is at prismmodelchecker.org/files/tacas22equ/     The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman and D. Parker Probabilistic Model Checking and Autonomy. Annual Review of Control, Robotics, and Autonomous Systems, volume 5, Annual Reviews. To appear, 2022. [pdf] [bib] Posted with permission from the Annual Review of Control, Robotics, and Autonomous Systems, copyright 2022 Annual Reviews.

2021

  • M. Kwiatkowska, G. Norman, D. Parker and G. Santos Automatic Verification of Concurrent Stochastic Systems. Formal Methods in System Design, Springer. January, 2021. [pdf] [bib] Supporting material is at prismmodelchecker.org/files/fmsd-csgs/ The original publication is available at SpringerLink
  • W. Kavanagh, A. Miller, G. Norman and O. Andrei. Balancing Turn-Based Games with Chained Strategy Generation. IEEE Transactions on Games, 13:(2):113-122, IEEE. June 2021. [bib]

2020

  • M. Kwiatkowska, G. Norman, D. Parker and G. Santos Multi-player Equilibria Verification for Concurrent Stochastic Games. In Proc. 17th International Conference on Quantitative Evaluation of Systems (QEST'20), volume 12289 of Lecture Notes in Computer Science, pages 74-95, Springer. August 2020. [pdf] [bib] An extended version of this paper, with complete proofs, is available at arxiv.org/abs/2007.03365
    Supporting material is at prismmodelchecker.org/files/qest20/     The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman, D. Parker and G. Santos PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time. In Proc. 32nd International Conference on Computer Aided Verification (CAV'20), Lecture Notes in Computer Science, volume 12225 of LNCS, pages 475-487, Springer. July 2020. [pdf] [bib] The original publication is available at SpringerLink
  • D. Fraser, R. Giaquinta, R. Hoffmann, M. Ireland, A. Miller and G. Norman Collaborative Models for Autonomous Systems Controller Synthesis. Formal Aspects of Computing, 32:157–186. April 2020. [pdf] [bib]

2019

  • M. Kwiatkowska, G. Norman, D. Parker and G. Santos. Equilibria-based Probabilistic Model Checking for Concurrent Stochastic Games. In Formal Methods – The Next 30 Years (FM'19), volume 11800 of Lecture Notes in Computer Science, pages 298-315, Springer. September 2019. [pdf] [bib] An extended version of this paper, with proofs, is available at arxiv.org/abs/1811.07145
    Supporting material (tool, source code, examples) is at prismmodelchecker.org/files/fm19nash/     The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman and D. Parker. Verification and Control of Turn-Based Probabilistic Real-Time Games. In The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy, volume 11760 of Lecture Notes in Computer Science, pages 379-396, Springer. November 2019. [pdf] [bib] An extended version of this paper, with complete proofs, is available at arxiv.org/abs/1906.09142.
    Supporting material is at prismmodelchecker.org/files/tptgs/.     The original publication is available at SpringerLink

2018

  • R. Giaquinta, R. Hoffmann, M. Ireland, A. Miller and G. Norman. Strategy Synthesis for Autonomous Agents using PRISM. In Proc. 10th NASA Formal Methods Symposium (NFM 2018), volume 10811 of Lecture Notes in Computer Science, pages 220-236, Springer. March 2018. [pdf] [bib] The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman, D. Parker and G. Santos. Automated Verification of Concurrent Stochastic Games. In Proc. 15th International Conference on Quantitative Evaluation of Systems (QEST'18), volume 11024 of Lecture Notes in Computer Science, pages 223-239, Springer. August 2018. [pdf] [bib] The original publication is available at SpringerLink

2017

  • M. Kwiatkowska, G. Norman and D. Parker. Symbolic Verification and Strategy Synthesis for Linearly-Priced Probabilistic Timed Automata. In Models, Algorithms, Logics and Tools, volume 10460 of Lecture Notes in Computer Science, pages 289-309, Springer. August 2017. [pdf] [bib] The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman and D. Parker. Probabilistic Model Checking: Advances and Applications. In R. Drechsler (editor), Formal System Verification, pages 73-121, Springer. June 2017. [pdf] [bib] The original publication is available at SpringerLink
  • G. Norman, D. Parker and X. Zou. Verification and Control of Partially Observable Probabilistic Systems. Real-Time Systems, 53(3):354-402, Springer. April 2017. [pdf] [bib] This is a journal version of [NPZ15].
  • A. Jovanovic, M Kwiatkowska, G. Norman and Q. Peyras. Symbolic Optimal Expected Time Reachability Computation and Controller Synthesis for Probabilistic Timed Automata. Theoretical Computer Science, Volume 669, Issue C, pages 1-21, Elsevier. March 2017. [pdf] [bib] This is a journal version of [JKN15].

2016

  • V. Forejt, M. Kwiatkowska, G. Norman and A. Trivedi. Expected Reachability-Time Games. Theoretical Computer Science, 631:139-160, Elsevier. June 2016. [pdf] [bib] This is a journal version of [FKNT10a] with complete proofs and several errors fixed.
  • R. Hoffmann, M. Ireland, A. Miller, G Norman and S. Veres. Autonomous Agent Behaviour Modelled in PRISM: A Case Study. In Proc. 23rd International SPIN Symposium on Model Checking of Software (SPIN’16), volume 9641 of Lecture Notes in Computer Science, pages 104-110, Springer. April 2016. [pdf] [bib] The original publication is available at SpringerLink

2015

  • A. Jovanovic, M Kwiatkowska and G. Norman. Symbolic Minimum Expected Time Controller Synthesis for Probabilistic Timed Automata. In Proc. 13th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'15), volume 9268 of Lecture Notes in Computer Science, pages 140-155, Springer. September 2015. [pdf] [bib] A full version of this paper, with proofs, can be found here. The original publication is available at SpringerLink
  • G. Norman, D. Parker and X. Zou. Verification and Control of Partially Observable Probabilistic Real-Time Systems. In Proc. 13th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'15), volume 9268 of Lecture Notes in Computer Science, pages 240-255, Springer. September 2015. [pdf] [bib] An extended version of this paper, with proofs, is available at arxiv.org/abs/1506.06419. The original publication is available at SpringerLink
  • Md Ferdous, G. Norman, A. Josang and R. Poet Mathematical Modelling of Trust Issues in Federated Identity Management. In Proceedings of Trust Management IX, Volume 454 of IFIP Advances in Information and Communication Technology, pages 13-29, Springer. April 2015. [pdf] [bib] The original publication is available at SpringerLink

2014

  • G. Norman and W. Sanders (editors) Proceedings 11th International Conference Quantitative Evaluation of Systems (QEST 2014). Volume 8657 of Lecture Notes in Computer Science. Springer. September 2014. [bib] The original publication is available at SpringerLink
  • G. Norman and D. Parker. Quantitative Verification: Formal Guarantees for Timeliness, Reliability and Performance. Mathematical knowledge transfer report by the London Mathematical Society and the Smith Institute. Edited by Robert Leese and Tom Melham. 2014. [pdf] [bib]
  • A. Abate, M. Kwiatkowska, G. Norman and D. Parker. Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations. In F. van Breugel, E. Kashefi, C. Palamidessi and J. Rutten (editors) Horizons of the Mind. A Tribute to Prakash Panangaden, volume 8464 of Lecture Notes in Computer Science, pages 40-58, Springer. May 2014. [pdf] [bib] The original publication is available at SpringerLink
  • M. Massink, G. Norman and H. Wiklicky (editors) Quantitative Aspects of Programming Languages. Theoretical Computer Science, Volume 538, Elsevier. June, 2014. [bib] The original publication is available at ScienceDirect
  • Md. Ferdous and G. Norman and R. Poet Mathematical Modelling of Identity, Identity Management and Other Related Topics. Proc. 7th Int. Conf. Security of Information and Networks (SIN'14). September 2014. [pdf] [bib] The original publication is available at ACM digital library

2013

  • M. Kwiatkowska, G. Norman, D. Parker and H. Qu. Compositional Probabilistic Verification through Multi-Objective Model Checking. Information and Computation, 232:38-65, Elsevier. November, 2013. [pdf] [bib]
  • G. Norman, D. Parker and J. Sproston Model Checking for Probabilistic Timed Automata. Formal Methods in System Design, 43(2):164-190, Springer. September, 2013. [pdf] [bib] Files for the case studies in the paper can be found here.
  • P. Biro and G. Norman Analysis of stochastic matching markets. International Journal of Game Theory, 42(4):1021-1040, Springer. November, 2013. [pdf] [bib] Further information and verification results also available from the PRISM case study page.
  • M. Duflot, M. Kwiatkowska, G. Norman, D. Parker, S. Peyronnet, C. Picaronny and J. Sproston. Practical Applications of Probabilistic Model Checking to Communication Protocols. In S. Gnesi and T. Margaria (editors) Formal Methods for Industrial Critical Systems: A Survey of Applications, pages 133-150, IEEE Computer Society Press March 2013. [pdf] [bib]

2012

  • P. Biro and G. Norman Analysis of stochastic matching markets. In Proc. 3rd Workshop Cooperative Games in Multiagent Systems (CoopMAS-2012). June, 2012. [pdf] [bib] Further information and verification results also available from the PRISM case study page
  • A. Di Pierro and G. Norman (editors) Quantitative Aspects of Programming Languages. Theoretical Computer Science, Volume 413, Elsevier. January, 2012. [bib] The original publication is available at ScienceDirect
  • M. Kwiatkowska, G. Norman and D. Parker. The PRISM Benchmark Suite. In Proc. 9th International Conference on Quantitative Evaluation of Systems (QEST'12), IEEE CS Press. 2012. [bib]
  • M. Kwiatkowska, G. Norman and D. Parker. Probabilistic Verification of Herman's Self-Stabilisation Algorithm. Formal Aspects of Computing, 24(4), pages 661-670, Springer. July 2012. [pdf] [bib]
  • J. Júlvez, M. Kwiatkowska, G. Norman and D. Parker. Evaluation of Sustained Stochastic Oscillations by Means of a System of Differential Equations. International Journal of Computers and Applications (IJCA), 19(2):101-111 2012. [pdf] [bib]

2011

  • M. Massink and G. Norman (editors) Proceedings of the 9th Workshop on Quantitative Aspects of Programming Languages (QAPL'11). Volume 57 of Electronic Proceedings in Theoretical Computer Science. EPTCS. 2011. [bib] The original publication is available at eptcs.org
  • E. M. Hahn, G. Norman, D. Parker, B. Wachter and L. Zhang. Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems. In Proc. 8th International Conference on Quantitative Evaluation of Systems (QEST'11), pages 69-78, IEEE CS Press. September 2011. [pdf] [bib]
  • M. Kwiatkowska, G. Norman and D. Parker. PRISM 4.0: Verification of Probabilistic Real-time Systems. In Proc. 23rd International Conference on Computer Aided Verification (CAV'11), volume 6806 of Lecture Notes in Computer Science, pages 585-591, Springer. July 2011. [pdf] [bib] The original publication is available at SpringerLink
  • V. Forejt, M. Kwiatkowska, G. Norman and D. Parker. Automated Verification Techniques for Probabilistic Systems. In M. Bernardo and V. Issarny (editors) Formal Methods for Eternal Networked Software Systems (SFM'11), volume 6659 of Lecture Notes in Computer Science, pages 53-113, Springer. June 2011. [pdf] [bib] The original publication is available at SpringerLink
  • V. Forejt, M. Kwiatkowska, G. Norman, D. Parker and H. Qu. Quantitative Multi-Objective Verification for Probabilistic Systems. In Proc. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11), volume 6605 of Lecture Notes in Computer Science, pages 112-127, Springer. March 2011. [pdf] [bib] A full version of this paper, with proofs, can be found here The original publication is available at SpringerLink
  • J. Júlvez, M. Kwiatkowska, G. Norman and D. Parker. A Systematic Approach to Evaluate Sustained Stochastic Oscillations. In H. Al-Mubaid (editor) Proc. ISCA 3rd International Conference on Bioinformatics and Computational Biology (BICoB'11), pages 134-139, ISCA. March 2011. [pdf] [bib]

2010

  • A. Di Pierro and G. Norman (editors) Proceedings of the 8th Workshop on Quantitative Aspects of Programming Languages (QAPL'10). Volume 28 of Electronic Proceedings in Theoretical Computer Science (EPTCS). 2010. [bib] The original publication is available at eptcs.org
  • M. Kwiatkowska, G. Norman and D. Parker. Advances and Challenges of Probabilistic Model Checking. In Proc. 48th Annual Allerton Conference on Communication, Control and Computing, pages 1691-1698, IEEE Press. Invited paper. October 2010. [pdf] [bib]
  • M. Kattenbelt, M. Kwiatkowska, G. Norman and D. Parker. A Game-based Abstraction-Refinement Framework for Markov Decision Processes. Formal Methods in System Design, 36(3), pages 246-280, Springer. September 2010. [pdf] [bib] The original publication is available at SpringerLink
  • V. Forejt, M. Kwiatkowska, G. Norman and A. Trivedi. Expected Reachability-Time Games. In K. Chatterjee and T. Henzinger (editors) Proeedings of 8th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'10), volume 6246 of Lecture Notes in Computer Science, pages 122-136, Springer. September 2010. [pdf] [bib] A full version of this paper, with proofs, can be found here The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman and D. Parker. A Framework for Verification of Software with Time and Probabilities. In Proc. 8th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'10), volume 6246 of Lecture Notes in Computer Science, pages 25-45, Springer. September 2010. [pdf] [bib] The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman and D. Parker. Probabilistic Model Checking for Systems Biology. In M. Sriram Iyengar (editor) Symbolic Systems Biology, pages 31-59, Jones and Bartlett. May 2010. [pdf] [bib]
  • M. Kwiatkowska, G. Norman, D. Parker and H. Qu. Assume-Guarantee Verification for Probabilistic Systems. In Proc. 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'10), volume 6015 of Lecture Notes in Computer Science, pages 23-37, Springer. March 2010. [pdf] [bib] A full version of this paper, with proofs, can be found here The original publication is available at SpringerLink

2009

  • M. Kwiatkowska, G. Norman and D. Parker. Stochastic Games for Verification of Probabilistic Timed Automata. In Proc. 7th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'09), volume 5813 of Lecture Notes in Computer Science, pages 212-227, Springer. September 2009. [pdf] [bib] A full version of this paper, with proofs, can be found here The original publication is available at SpringerLink
  • M. Jurdzinski, M. Kwiatkowska, G. Norman and A. Trivedi. Concavely-Priced Probabilistic Timed Automata. In M. Bravetti and G. Zavattaro (editors) Proc. 20th Int. Conf. Concurrency Theory (CONCUR'09), volume 5710 of Lecture Notes in Computer Science, pages 415-430, Springer. September 2009. [pdf] [bib] A full version of this paper, with proofs, can be found here The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman and D. Parker. Quantitative Verification Techniques for Biological Processes. In A. Condon, D. Harel, J. Kok, A. Salomaa and E. Winfree (editors) Algorithmic Bioprocesses, pages 391-409, Springer. August 2009. [pdf] [bib] The original publication is available at SpringerLink
  • G. Norman, C. Palamidessi, D. Parker and P. Wu. Model Checking Probabilistic and Stochastic Extensions of the Pi-Calculus. IEEE Transactions on Software Engineering, 35(2), pages 209-223, IEEE Computer Society. March 2009. [pdf] [bib]
  • M. Kwiatkowska, G. Norman, D. Parker and M.G. Vigliotti. Probabilistic Mobile Ambients. Theoretical Computer Science, 410(12-13), pages 1272-1303, Elsevier. March 2009. [pdf] [bib]
  • K. Chatzikokolakis, G. Norman and D. Parker. Bisimulation for Demonic Schedulers. In Proc. 12th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'09), volume 5504 of Lecture Notes in Computer Science, pages 318-332, Springer. March 2009. [pdf] [bib] The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman and D. Parker. PRISM: Probabilistic Model Checking for Performance and Reliability Analysis. ACM SIGMETRICS Performance Evaluation Review, 36(4), pages 40-45, ACM. March 2009. [pdf] [bib]
  • M. Kattenbelt, M. Kwiatkowska, G. Norman and D. Parker. Abstraction Refinement for Probabilistic Software. In Proc. 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'09), volume 5403 of Lecture Notes in Computer Science, pages 182-197, Springer. January 2009. [pdf] [bib] The case studies used in this paper can be found here The original publication is available at SpringerLink

2008

  • M. Kwiatkowska, G. Norman and D. Parker. Analysis of a Gossip Protocol in PRISM. ACM SIGMETRICS Performance Evaluation Review, 36(3), pages 17-22. December 2008. [pdf] [bib]
  • P. Roy, D. Parker, G. Norman and L. de Alfaro. Symbolic Magnifying Lens Abstraction in Markov Decision Processes. In Proc. 5th International Conference on Quantitative Evaluation of Systems (QEST'08), pages 103-112, IEEE CS Press. September 2008. [pdf] [bib]
  • M. Kattenbelt, M. Kwiatkowska, G. Norman and D. Parker. Game-Based Probabilistic Predicate Abstraction in PRISM. In Proc. 6th Workshop on Quantitative Aspects of Programming Languages (QAPL'08), volume 220 (3) of Electronic Notes in Theoretical Computer Science , pages 5-21 , Elsevier. March 2008. [pdf] [bib] A full version of this paper, with proofs, can be found here
  • M. Kwiatkowska, G. Norman and D. Parker. Using Probabilistic Model Checking in Systems Biology. ACM SIGMETRICS Performance Evaluation Review, 35(4), pages 14-21, Association for Computing Machinery. March 2008. [pdf] [bib]
  • J. Heath, M. Kwiatkowska, G. Norman, D. Parker and O. Tymchyshyn. Probabilistic Model Checking of Complex Biological Pathways. Theoretical Computer Science (Special Issue on Converging Sciences: Informatics and Biology), 391(3), pages 239-257, Elsevier. February 2008. [pdf] [bib] Supplementary material available at supporting website: qav.comlab.ox.ac.uk/projects/sysbio/fgf.php Further information and verification results also available from the PRISM case study page
  • M. Kwiatkowska, G. Norman, D. Parker and J. Sproston. Verification of Real-Time Probabilistic Systems. In S. Merz and N. Navet (editors) Modeling and Verification of Real-Time Systems: Formalisms and Software Tools, pages 249-288, John Wiley & Sons. January 2008. [pdf] [bib] The original publication is available at iste

2007

  • M. Kwiatkowska, G. Norman and D. Parker. Controller Dependability Analysis By Probabilistic Model Checking. Control Engineering Practice, 15(11), pages 1427-1434, Elsevier. November 2007. [pdf] [bib]
  • G. Norman, C. Palamidessi, D. Parker and P. Wu. Model Checking the Probabilistic Pi-calculus. In Proc. 4th International Conference on Quantitative Evaluation of Systems (QEST'07), pages 169-178, IEEE CS Press. September 2007. [pdf] [bib] A full version of this paper, with proofs, can be found here
  • M. Kwiatkowska, G. Norman, J. Sproston and F. Wang. Symbolic Model Checking for Probabilistic Timed Automata. Information and Computation, 205(7), pages 1027-1077. July 2007. [pdf] [bib]
  • M. Kwiatkowska, G. Norman and D. Parker. Stochastic Model Checking. In M. Bernardo and J. Hillston (editors) Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07), volume 4486 of Lecture Notes in Computer Science (Tutorial Volume), pages 220-270, Springer. June 2007. [pdf] [bib] The original publication is available at SpringerLink

2006

  • M. Groesser, G. Norman, C. Baier, F. Ciesinski, M. Kwiatkowska, D. Parker. On reduction criteria for probabilistic reward models. In S. Arun-Kumar and N. Garg (editors) Proc. 25th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'06), volume 4337 of Lecture Notes in Computer Science, pages 309-320, Springer Verlag. December 2006. [pdf] [bib] The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman, D. Parker, O. Tymchyshyn, J. Heath and E. Gaffney. Simulation and Verification for Computational Modelling of Signalling Pathways. In Proc. 2006 Winter Simulation Conference, pages 1666-1674. December 2006. [pdf] [bib]
  • M. Duflot, M. Kwiatkowska, G. Norman and D. Parker. A Formal Analysis of Bluetooth Device Discovery. International Journal on Software Tools for Technology Transfer (STTT), 8(6), pages 621 - 632, Springer-Verlag. November 2006. [pdf] [bib] For further details of this case study, see the PRISM case study page The original publication is available at SpringerLink
  • G. Norman and V. Shmatikov. Analysis of Probabilistic Contract Signing. Journal of Computer Security, 14(6), pages 561-589, IOS Press. November 2006. [pdf] [bib] For further details of this case study, see the PRISM case study page
  • J. Heath, M. Kwiatkowska, G. Norman, D. Parker and O. Tymchyshyn. Probabilistic model checking of complex biological pathways. In C. Priami (editor) Proc. Computational Methods in Systems Biology (CMSB'06), volume 4210 of Lecture Notes in Bioinformatics, pages 32-47, Springer Verlag. October 2006. [pdf] [bib] The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman and D. Parker. Game-based Abstraction for Markov Decision Processes. In Proc. 3rd International Conference on Quantitative Evaluation of Systems (QEST'06), pages 157-166, IEEE CS Press. Winner of the QEST'06 Best Paper Award. September 2006. [pdf] [bib] A full version of this paper, with proofs, can be found here
  • M. Kwiatkowska, G. Norman and D. Parker. Symmetry Reduction for Probabilistic Model Checking. In T. Ball and R. Jones (editors) Proc. 18th International Conference on Computer Aided Verification (CAV'06), volume 4144 of Lecture Notes in Computer Science, pages 234-248, Springer-Verlag. August 2006. [pdf] [bib] The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman, D. Parker and J. Sproston. Performance Analysis of Probabilistic Timed Automata using Digital Clocks. Formal Methods in System Design, 29, pages 33-78, Springer. August 2006. [pdf] [bib] The original publication is available at SpringerLink
  • H. Younes, M. Kwiatkowska, G. Norman and D. Parker. Numerical vs. Statistical Probabilistic Model Checking. International Journal on Software Tools for Technology Transfer (STTT), 8(3), pages 216-228, Springer. June 2006. [pdf] [bib] The original publication is available at SpringerLink
  • A. Hinton, M. Kwiatkowska, G. Norman and D. Parker. PRISM: A Tool for Automatic Verification of Probabilistic Systems. In H. Hermanns and J. Palsberg (editors) Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06), volume 3920 of Lecture Notes in Computer Science, pages 441-444, Springer. March 2006. [pdf] [bib] The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman and A. Pacheco. Model Checking Expected Time and Expected Reward Formulae with Random Time Bounds. Computers & Mathematics with Applications, 51(2), pages 305-316, Elsevier. January 2006. [pdf] [bib]

2005

  • G. Norman, D. Parker, M. Kwiatkowska and S. Shukla. Evaluating the Reliability of NAND Multiplexing with PRISM. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 24(10), pages 1629-1637. October 2005. [pdf] [bib] For further details of this case study, see the PRISM case study page
  • M. Kwiatkowska, G. Norman and D. Parker. Probabilistic Model Checking and Power-Aware Computing. In In Proc. 7th International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS), pages 6-9. September 2005. [pdf] [bib]
  • G. Norman, D. Parker, M. Kwiatkowska, S. Shukla and R. Gupta. Using Probabilistic Model Checking for Dynamic Power Management. Formal Aspects of Computing, 17(2), pages 160-176, Springer-Verlag. August 2005. [pdf] [bib] For further details of this case study, see the PRISM case study page The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman and D. Parker. Quantitative Analysis with the Probabilistic Model Checker PRISM. Electronic Notes in Theoretical Computer Science, 153(2), pages 5-31, Elsevier. May 2005. [pdf] [bib]
  • S. Cattani, R. Segala, M. Kwiatkowska and G. Norman. Stochastic transition systems for continuous state spaces and non-determinism. In V. Sassone (editor) Proc. Foundations of Software Science and Computation Structures (FOSSACS'05), volume 3441 of Lecture Notes in Computer Science, pages 125-139, Springer Verlag. April 2005. [pdf] [bib] The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman and D. Parker. Probabilistic Model Checking in Practice: Case Studies with PRISM. ACM SIGMETRICS Performance Evaluation Review, 32(4), pages 16-21. March 2005. [pdf] [bib]

2004

  • M. Duflot, M. Kwiatkowska, G. Norman and D. Parker. A Formal Analysis of Bluetooth Device Discovery. In T. Margaria and B. Steffen, A. Philippou and M. Reitenspiess (editors) Proc. 1st International Symposium on Leveraging Applications of Formal Methods (ISOLA'04), volume TR-2004-6 of Technical Report, pages 268-275, Department of Computer Science, University of Cyprus. November 2004. [pdf] [bib]
  • G. Norman. Analysing Randomized Distributed Algorithms. In C. Baier, B. Haverkort, H. Hermanns, J-P. Katoen, M. Siegle and F. Vaandrager (editors) Validation of Stochastic Systems: A Guide to Current Research, volume 2925 of Lecture Notes in Computer Science, pages 384-418, Springer. October 2004. [pdf] [bib] The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman, J. Sproston and F. Wang. Symbolic Model Checking for Probabilistic Timed Automata. In Y. Lakhnech and S. Yovine (editors) Proc. FORMATS/FTRTFT'04, volume 3253 of Lecture Notes in Computer Science, pages 293-308, Springer. September 2004. [pdf] [bib] The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman and D. Parker. Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach. International Journal on Software Tools for Technology Transfer (STTT), 6(2), pages 128-142. September 2004. [pdf] [bib]
  • M. Kwiatkowska, G. Norman and D. Parker. PRISM 2.0: A Tool for Probabilistic Model Checking. In Proc. 1st International Conference on Quantitative Evaluation of Systems (QEST'04), pages 322-323, IEEE CS Press. September 2004. [pdf] [bib]
  • M. Kwiatkowska, G. Norman and D. Parker. Controller Dependability Analysis By Probabilistic Model Checking. In Proc. 11th IFAC Symposium on Information Control Problems in Manufacturing (INCOM'04), pages 177-182, Elsevier. April 2004. [pdf] [bib]
  • H. Younes, M. Kwiatkowska, G. Norman and D. Parker. Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study. In K. Jensen and A. Podelski (editors) Proc. TACAS'04, volume 2988 of Lecture Notes in Computer Science, pages 46-60, Springer. March 2004. [pdf] [bib] The original publication is available at SpringerLink
  • J. Rutten, M. Kwiatkowska, G. Norman and D. Parker. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. Volume 23 of CRM Monograph Series. American Mathematical Society. P. Panangaden and F. van Breugel (eds.). March 2004. [bib]
  • C. Daws, M. Kwiatkowska and G. Norman. Automatic Verification of the IEEE 1394 Root Contention Protocol with KRONOS and PRISM. International Journal on Software Tools for Technology Transfer (STTT), 5(2), pages 221-236. March 2004. [pdf] [bib]
  • G. Norman, D. Parker, M. Kwiatkowska and S. Shukla. Evaluating the Reliability of Defect-Tolerant Architectures for Nanotechnology with Probabilistic Model Checking. In Proc. International Conference on VLSI Design, pages 907-914, IEEE CS Press. January 2004. [pdf] [bib]

2003

  • M. Kwiatkowska, G. Norman and J. Sproston. Symbolic Model Checking for Probabilistic Timed Automata. Technical report CSR-03-10, School of Computer Science, University of Birmingham. October 2003. [pdf] [bib]
  • M. Kwiatkowska, G. Norman, D. Parker and J. Sproston. Performance Analysis of Probabilistic Timed Automata using Digital Clocks. In Proc. Formal Modeling and Analysis of Timed Systems (FORMATS'03), volume 2791 of Lecture Notes in Computer Science, pages 105-120, Springer. September 2003. [pdf] [bib] The original publication is available at SpringerLink
  • H. Hermanns, M. Kwiatkowska, G. Norman, D. Parker and M. Siegle. On the use of MTBDDs for Performability Analysis and Verification of Stochastic Systems. Journal of Logic and Algebraic Programming: Special Issue on Probabilistic Techniques for the Design and Analysis of Systems, 56, pages 23-67, Elsevier. June 2003. [pdf] [bib]
  • M. Kwiatkowska, G. Norman and J. Sproston. Probabilistic Model Checking of Deadline Properties in the IEEE1394 FireWire Root Contention Protocol. Formal Aspects of Computing, 14(3), pages 295-318. April 2003. [pdf] [bib]
  • M. Kwiatkowska, G. Norman and J. Sproston. PCTL model checking of symbolic probabilistic systems. Technical report CSR-03-2, University of Birmingham, School of Computer Science. April 2003. [pdf] [bib]
  • G. Norman, D. Parker, M. Kwiatkowska, S. Shukla and R. Gupta. Using Probabilistic Model Checking for Dynamic Power Management. In Proc. 3rd Workshop on Automated Verification of Critical Systems (AVoCS'03). Technical Report DSSE-TR-2003-2, University of Southampton. April 2003. [pdf] [bib]
  • M. Kwiatkowska, G. Norman and J. Sproston. Symbolic Computation of Minimal Probabilistic Reachability. Technical report CSR-03-01, University of Birmingham, School of Computer Science. January 2003. [pdf] [bib]

2002

  • G. Norman and V. Shmatikov. Analysis of Probabilistic Contract Signing. In A. Abdallah, P. Ryan and S. Schneider (editors) Proc. BCS-FACS Formal Aspects of Security (FASec'02), volume 2629 of Lecture Notes in Computer Science, pages 81-96, Springer. December 2002. [pdf] [bib] The original publication is available at SpringerLink
  • M. Kwiatkowska and G. Norman. Verifying Randomized Byzantine Agreement. In D. Peled and M. Vardi (editors) Proc. Formal Techniques for Networked and Distributed Systems (FORTE'02), volume 2529 of Lecture Notes in Computer Science, pages 194-209, Springer. November 2002. [pdf] [bib] The original publication is available at SpringerLink
  • G. Norman, M. Kwiatkowska, D. Parker, S. Shukla and R. Gupta. Formal Analysis and Validation of Continuous Time Markov Chain Based System Level Power Management Strategies. In Proc. 7th Annual IEEE International Workshop on High Level Design Validation and Test (HLDVT'02), pages 45-50, OmniPress. October 2002. [pdf] [bib]
  • M. Kwiatkowska, G. Norman and A. Pacheco. Model Checking Expected Time and Expected Reward Formulae with Random Time Bounds. In Proc. 2nd Euro-Japanese Workshop on Stochastic Risk Modelling for Finance, Insurance, Production and Reliability. September 2002. [pdf] [bib]
  • M. Kwiatkowska, R. Mehmood, G. Norman and D. Parker. A Symbolic Out-of-Core Solution Method for Markov Models. In Proc. Workshop on Parallel and Distributed Model Checking (PDMC'02), volume 68.4 of ENTCS. August 2002. [pdf] [bib]
  • C. Daws, M. Kwiatkowska and G. Norman. Automatic Verification of the IEEE 1394 Root Contention Protocol with KRONOS and PRISM. In Proc. 7th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'02), volume 66.2 of ENTCS. July 2002. [pdf] [bib]
  • M. Kwiatkowska, G. Norman and A. Pacheco. Model Checking CSL Until Formulae with Random Time Bounds. In H. Hermanns and R. Segala (editors) Proc. PAPM/PROBMIV'02, volume 2399 of Lecture Notes in Computer Science, pages 152-168, Springer. July 2002. [pdf] [bib] The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman and J. Sproston. Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol. In H. Hermanns and R. Segala (editors) Proc. PAPM/PROBMIV'02, volume 2399 of Lecture Notes in Computer Science, pages 169-187, Springer. July 2002. [pdf] [bib] The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman, R. Segala and J. Sproston. Automatic Verification of Real-time Systems with Discrete Probability Distributions. Theoretical Computer Science, 282, pages 101-150. June 2002. [pdf] [bib]
  • M. Kwiatkowska, G. Norman and D. Parker. PRISM: Probabilistic Symbolic Model Checker. In T. Field, P. Harrison, J. Bradley and U. Harder (editors) Proc. TOOLS 2002, volume 2324 of Lecture Notes in Computer Science, pages 200-204, Springer. April 2002. [pdf] [bib] The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman and D. Parker. Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach. In J-P. Katoen and P. Stevens (editors) Proc. TACAS'02, volume 2280 of Lecture Notes in Computer Science, pages 52-66, Springer. April 2002. [pdf] [bib] The original publication is available at SpringerLink

2001

  • J.-P. Katoen, M. Kwiatkowska, G. Norman and D. Parker. Faster and Symbolic CTMC Model Checking. In L. de Alfaro and S. Gilmore (editors) Proc. PAPM/PROBMIV'01, volume 2165 of Lecture Notes in Computer Science, pages 23-38, Springer. September 2001. [pdf] [bib] The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman and D. Parker. PRISM: Probabilistic Symbolic Model Checker. In Proc. PAPM/PROBMIV'01 Tools Session, pages 7-12. Available as Technical Report 760/2001, University of Dortmund. September 2001. [pdf] [bib]
  • M. Kwiatkowska, G. Norman and J. Sproston. Symbolic computation of maximal probabilistic reachability. In K. Larsen and M. Nielsen (editors) Proc. 13th International Conference on Concurrency Theory (CONCUR'01), volume 2154 of Lecture Notes in Computer Science, pages 169-183, Springer. August 2001. [pdf] [bib] The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman and R. Segala. Automated Verification of a Randomised Distributed Consensus Protocol Using Cadence SMV and PRISM. In G. Berry, H. Common and A. Finkel (editors) Proc. CAV'01, volume 2102 of Lecture Notes in Computer Science, pages 194-206, Springer. January 2001. [pdf] [bib] The original publication is available at SpringerLink

2000

  • M. Kwiatkowska, G. Norman, R. Segala and J. Sproston. Verifying Quantitative Properties of Continuous Probabilistic Timed Automata. In C. Palamidessi (editor) Proc. CONCUR 2000 - Concurrency Theory, volume 1877 of Lecture Notes in Computer Science, pages 123-137, Springer. August 2000. [pdf] [bib] The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman and D. Parker. Verifying Randomized Distributed Algorithms with PRISM. In Proc. Workshop on Advances in Verification (Wave'2000). July 2000. [pdf] [bib]
  • M. Kwiatkowska, G. Norman, R. Segala and J. Sproston. Verifying Soft Deadlines with Probabilistic Timed Automata. In Proc. Workshop on Advances in Verification (Wave'2000). July 2000. [pdf] [bib]
  • L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker and R. Segala. Symbolic Model Checking of Probabilistic Processes using MTBDDs and the Kronecker Representation. In S. Graf and M. Schwartzbach (editors) Proc. TACAS'00, volume 1785 of Lecture Notes in Computer Science, pages 395-410, Springer. March 2000. [pdf] [bib] The original publication is available at SpringerLink
  • M. Kwiatkowska, G. Norman and J. Sproston. Symbolic Model Checking of Probabilistic Timed Automata Using Backwards Reachability. Technical report CSR-00-01, University of Birmingham, School of Computer Science. January 2000. [pdf] [bib]

1999

  • A. El-Rayes, M. Kwiatkowska and G. Norman. Solving Infinite Stochastic Process Algebra Models Through Matrix-Geometric Methods. In J. Hillston and M. Silva (editors) Proc. 7th Process Algebras and Performance Modelling Workshop (PAPM'99), pages 41-62, University of Zaragoza. September 1999. [pdf] [bib]
  • C. Baier, M. Kwiatkowska and G. Norman. Computing Probability Lower and Upper Bounds for LTL Formulae over Sequential and Concurrent Markov Chains. In C. Baier and M. Huth and M. Kwiatkowska and M. Ryan (editors) Proc. 1st Probabilistic Methods in Verification Workshop (PROBMIV'98), volume 22 of Electronic Notes in Theoretical Computer Science, Elsevier Science. June 1999. [pdf] [bib]
  • M. Kwiatkowska, G. Norman, R. Segala and J. Sproston. Automatic Verification of Real-Time Systems with Discrete Probability Distributions. In J.-P. Katoen (editor) Proc. 5th International AMAST Workshop on Real-Time and Probabilistic Systems (ARTS'99), volume 1601 of Lecture Notes in Computer Science, pages 75-95, Springer. March 1999. [pdf] [bib] The original publication is available at SpringerLink

1998

  • M. Kwiatkowska and G. Norman. A Testing Equivalence for Reactive Probabilistic Processes. In A Testing Equivalence for Reactive Probabilistic Processes , volume 16(2) of Electronic Notes in Theoretical Computer Science, pages 114-132, Elsevier Science. September 1998. [pdf] [bib]
  • M. Kwiatkowska and G. Norman. A Fully Abstract Metric-Space Denotational Semantics for Reactive Probabilistic Processes. In Proc. 3rd Workshop on Computation and Approximation (Comprox III), volume 13 of Electronic Notes in Theoretical Computer Science, Elsevier Science. September 1998. [pdf] [bib]

1997

  • G. Norman. Metric Semantics for Reactive Probabilistic Processes. Ph.D. thesis, School of Computer Science, University of Birmingham. November 1997. [pdf] [bib]

1996

  • M. Kwiatkowska and G. Norman. Probabilistic Metric Semantics for a Simple Language with Recursion. In W. Penczek and A. Szalas (editors) Proc. 21st International Symposium on Mathematical Foundations of Computer Science (MFCS'96), volume 1113 of Lecture Notes in Computer Science, pages 419-430, Springer. September 1996. [pdf] [bib] The original publication is available at SpringerLink
  • M. Kwiatkowska and G. Norman. Metric Denotational Semantics for PEPA. In M. Ribaudo (editor) Proc. 4th Process Algebras and Performance Modelling Workshop (PAPM'96), pages 120-138, CLUT. July 1996. [pdf] [bib]