Dr Gethin Norman
- Senior Lecturer (Computing Science)
telephone:
0141 330 1630
email:
Gethin.Norman@glasgow.ac.uk
S124, Computing Science, Sir Alwyn Williams Bldg, Glasgow G12 8QQ
Biography
I am a Scottish Informatics and Computer Science Alliance (SICSA) senior lecturer in the School of Computing Science at the University of Glasgow and member of the formal methods research group which is part of the Formal Analysis, Theory and Algorithms research section. I was the co-leader of SICSA's Modelling and Abstraction research theme between 2012-16. Currently I am the deputy head of school and head of honours.
Previously I obtained a degree in mathematics from the University of Oxford and a PhD in computer science from the University of Birmingham. Between 1998 and 2007 I was a Research Fellow in the School of Computer Science at the University of Birmingham and from July 2007 until November 2009, a research officer in the Oxford University Computing Laboratory.
Research interests
My research is within the field of formal verification with emphasis on quantitative formal methods, particularly models and algorithms for systems exhibiting real-time and probabilistic behaviour. My interests within this field includes its application to software, security protocols and biological systems, as well as techniques for abstraction and refinement, compositional analysis and using game theory.
I am one of the principal developers for the probabilistic verification tool PRISM and its extension to game-based models PRISM-games. PRISM is a software tool for the modelling and analysis of systems whose behaviour exhibits uncertainty or randomness. Example applications include the analysis of the safety of a car's airbag control system, the performance of a Bluetooth-enabled wireless devices and thebehaviour of proteins in a cell. The tool has been used by researchers across the world from fields such as security, robotics, systems biology and quantum cryptography.
Together with Marta Kwiatkowska (University of Oxford) and David Parker (University of Birmingham) we were given the 2016 HVC award for "the invention, development and maintenance of the PRISM probabilistic model checker". The HVC award is given to the most influential work in the last five years in formal verification, simulation, and testing. The committee recognised our "outstanding contributions to probabilistic model checking and, more generally, to formal verification".
Find out more on my personal website.
Publications
Selected publications
Kwiatkowska, M., Norman, G. , Parker, D. and Santos, G. (2019) Equilibria-based probabilistic model checking for concurrent stochastic games. In: ter Beek, M. H., McIver, A. and Oliveira, J. N. (eds.) Formal Methods - The Next 30 Years. Series: Lecture Notes in Computer Science (11800). Springer, pp. 298-315. ISBN 9783030309411 (doi: 10.1007/978-3-030-30942-8_19)
Norman, G. , Parker, D. and Zou, X. (2017) Verification and control of partially observable probabilistic systems. Real-Time Systems, 53(3), pp. 354-402. (doi: 10.1007/s11241-017-9269-4)
Kwiatkowska, M., Norman, G. , Parker, D. and Santos, G. (2018) Automated verification of concurrent stochastic games. In: 15th International Conference on Quantitative Evaluation of SysTems (QEST 2018), Beijing, China, 04-07 Sept 2018, pp. 223-239. ISBN 9783319991535 (doi: 10.1007/978-3-319-99154-2_14)
Jovanovic, A., Kwiatkowska, M., Norman, G. and Peyras, Q. (2017) Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata. Theoretical Computer Science, 669, pp. 1-21. (doi: 10.1016/j.tcs.2017.01.015)
Norman, G. and Parker, D. (2014) Quantitative Verification: Formal Guarantees for Timeliness, Reliability and Performance. Technical Report. London Mathematical Society and Smith Institute.
Kwiatkowska, M., Norman, G. , Parker, D. and Qu, H. (2013) Compositional probabilistic verification through multi-objective model checking. Information and Computation, 232(6), pp. 38-65. (doi: 10.1016/j.ic.2013.10.001)
All publications
2024
Yan, R., Santos, G., Norman, G. , Parker, D. and Kwiatkowska, M. (2024) Strategy synthesis for zero-sum neuro-symbolic concurrent stochastic games. Information and Computation, 300, 105193. (doi: 10.1016/j.ic.2024.105193) (Accepted for Publication)
Yan, R., Santos, G., Norman, G. , Parker, D. and Kwiatkowska, M. (2024) Partially Observable Stochastic Games with Neural Perception Mechanisms. In: 26th International Symposium on Formal Methods (FM24), Milan, Italy, 11-13 September 2024, (Accepted for Publication)
Yan, R., Santos, G., Norman, G. , Parker, D. and Kwiatkowska, M. (2024) HSVI-based Online Minimax Strategies for Partially Observable Stochastic Games with Neural Perception Mechanisms. In: 2024 Learning for Dynamics and Control Conference (L4DC), Oxford, UK, 15-17 July, 2024, (Accepted for Publication)
2022
Kwiatkowska, M., Norman, G. , Parker, D., Santos, G. and Yang, R. (2022) Probabilistic Model Checking for Strategic Equilibria-based Decision Making: Advances and Challenges. In: 47th International Symposium on Mathematical Foundations of Computer Science, Vienna, Austria, 22-26 Aug 2022, p. 4. ISBN 9783959772563 (doi: 10.4230/LIPIcs.MFCS.2022.4)
Kavanagh, W., Fraser, D., Hunter, E. , Pancheva, A., Parkinson, J. , Paun, I., Wallis, T. , Ada, M. B., Border, H. and Norman, G. (2022) Experience report: challenges and opportunities of remote labs for a computer science department. Postgraduate Pedagogies, 2(1), pp. 173-207.
Kwiatkowska, M., Norman, G. and Parker, D. (2022) Probabilistic model checking and autonomy. Annual Review of Control, Robotics, and Autonomous Systems, 5, (doi: 10.1146/annurev-control-042820-010947)
Kwiatkowska, M., Norman, G. , Parker, D. and Santos, G. (2022) Correlated Equilibria and Fairness in Concurrent Stochastic Games. In: 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'22), Munich, Germany, 02-07 Apr 2022, pp. 60-78. ISBN 978-3-030-99527-0 (doi: 10.1007/978-3-030-99527-0_4)
Kwiatkowska, M., Norman, G. , Parker, D. and Santos, G. (2022) Symbolic verification and strategy synthesis for turn-based stochastic games. In: Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday. Series: Lecture Notes In Computer 13660. Springer. (Accepted for Publication)
2021
Kwiatkowska, M., Norman, G. , Parker, D. and Santos, G. (2021) Automatic verification of concurrent stochastic systems. Formal Methods in System Design, 58(1-2), pp. 188-250. (doi: 10.1007/s10703-020-00356-y)
Kavanagh, W. , Miller, A. , Norman, G. and Andrei, O. (2021) Balancing turn-based games with chained strategy generation. IEEE Transactions on Games, 13(2), pp. 113-122. (doi: 10.1109/TG.2019.2943227)
2020
Fraser, D., Giaquinta, R., Hoffmann, R., Ireland, M., Miller, A. and Norman, G. (2020) Collaborative models for autonomous systems controller synthesis. Formal Aspects of Computing, 32, pp. 157-186. (doi: 10.1007/s00165-020-00508-1)
Kwiatkowska, M., Norman, G. , Parker, D. and Santos, G. (2020) Multi-player Equilibria Verification for Concurrent Stochastic Games. In: 17th International Conference on Quantitative Evaluation of SysTems (QEST 2020), 31 Aug - 03 Sep 2020, ISBN 9783030598532 (doi: 10.1007/978-3-030-59854-9_7)
2019
Kwiatkowska, M., Norman, G. and Parker, D. (2019) Verification and Control of Turn-Based Probabilistic Real-Time Games. In: Alvim, M. S., Chatzikokolakis, K., Olarte, C. and Valencia, F. (eds.) The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy: Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday. Series: Lecture notes in computer science (11760). Springer: Cham, pp. 379-396. ISBN 9783030311742 (doi: 10.1007/978-3-030-31175-9_22)
Kwiatkowska, M., Norman, G. , Parker, D. and Santos, G. (2019) Equilibria-based probabilistic model checking for concurrent stochastic games. In: ter Beek, M. H., McIver, A. and Oliveira, J. N. (eds.) Formal Methods - The Next 30 Years. Series: Lecture Notes in Computer Science (11800). Springer, pp. 298-315. ISBN 9783030309411 (doi: 10.1007/978-3-030-30942-8_19)
2018
Kwiatkowska, M., Norman, G. , Parker, D. and Santos, G. (2018) Automated verification of concurrent stochastic games. In: 15th International Conference on Quantitative Evaluation of SysTems (QEST 2018), Beijing, China, 04-07 Sept 2018, pp. 223-239. ISBN 9783319991535 (doi: 10.1007/978-3-319-99154-2_14)
Scott, P. H., Veitch, N. J. , Gadegaard, H., Mughal, M., Norman, G. and Welsh, M. (2018) Enhancing theoretical understanding of a practical biology course using active and self-directed learning strategies. Journal of Biological Education, 52(2), pp. 184-195. (doi: 10.1080/00219266.2017.1293557)
Giaquinta, R., Hoffmann, R., Ireland, M. , Miller, A. and Norman, G. (2018) Strategy Synthesis for Autonomous Agents Using PRISM. In: 10th NASA Formal Methods Symposium (NFM 2018), Newport News, VA, USA, 17-19 Apr 2018, pp. 220-236. ISBN 9783319779348 (doi: 10.1007/978-3-319-77935-5_16)
2017
Kwiatkowska, M., Norman, G. and Parker, D. (2017) Symbolic Verification and Strategy Synthesis for Linearly-Priced Probabilistic Timed Automata. In: KiMfest: A Conference in Honour of Kim G. Larsen on the Occasion of his 60th Birthday, Aalborg University, Denmark, 19-20 Aug 2017, pp. 289-309. ISBN 9783319631202 (doi: 10.1007/978-3-319-63121-9_15)
Norman, G. , Parker, D. and Zou, X. (2017) Verification and control of partially observable probabilistic systems. Real-Time Systems, 53(3), pp. 354-402. (doi: 10.1007/s11241-017-9269-4)
Jovanovic, A., Kwiatkowska, M., Norman, G. and Peyras, Q. (2017) Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata. Theoretical Computer Science, 669, pp. 1-21. (doi: 10.1016/j.tcs.2017.01.015)
Kwiatkowska, M., Norman, G. and Parker, D. (2017) Probabilistic model checking: advances and applications. In: Drechsler, R. (ed.) Formal System Verification: State-of the-Art and Future Trends. Springer Verlag, pp. 73-121. ISBN 9783319576831 (doi: 10.1007/978-3-319-57685-5_3)
2016
Forejt, V., Kwiatkowska, M., Norman, G. and Trivedi, A. (2016) Expected reachability-time games. Theoretical Computer Science, 631, pp. 139-160. (doi: 10.1016/j.tcs.2016.04.021)
Hoffmann, R., Ireland, M. , Miller, A. , Norman, G. and Veres, S. (2016) Autonomous agent behaviour modelled in PRISM: a case study. Lecture Notes in Computer Science, 9641, pp. 104-110. (doi: 10.1007/978-3-319-32582-8_7)
2015
Ferdous, M. S., Norman, G. , Jøsang, A. and Poet, R. (2015) Mathematical modelling of trust issues in federated identity management. In: Damsgaard Jensen, C., Marsh, S., Dimitrakos, T. and Murayama, Y. (eds.) Trust Management IX: 9th Ifip Wg 11.11 International Conference, Ifiptm 2015, Hamburg, Germany, May 26-28, 2015, Proceedings. Series: IFIP Advances in Information and Communication Technology (454). Springer International Publishing, pp. 13-29. ISBN 9783319184906 (doi: 10.1007/978-3-319-18491-3_2)
Jovanovic, A., Norman, G. and Kwiatkowska, M. (2015) Symbolic Minimum Expected Time Controller Synthesis for Probabilistic Timed Automata. Lecture Notes in Computer Science, 9268, pp. 140-155. (doi: 10.1007/978-3-319-22975-1_10)
Norman, G. , Parker, D. and Zou, X. (2015) Verification and Control of Partially Observable Probabilistic Real-Time Systems. Lecture Notes in Computer Science, 9268, pp. 240-255. (doi: 10.1007/978-3-319-22975-1_16)
2014
Norman, G. and William, S. eds. (2014) Quantitative Evaluation of Systems: 11th International Conference, Florence, Italy, 8-10 September 2014. Series: Lecture Notes in Computer Science, 8657. Springer Verlag. ISBN 9783319106960
Abate, A., Kwiatkowska, M., Norman, G. and Parker, D. (2014) Probabilistic model checking of labelled Markov processes via finite approximate bisimulations. Lecture Notes in Computer Science, 8464, pp. 40-58. (doi: 10.1007/978-3-319-06880-0_2)
Norman, G. and Parker, D. (2014) Quantitative Verification: Formal Guarantees for Timeliness, Reliability and Performance. Technical Report. London Mathematical Society and Smith Institute.
2013
Biro, P. and Norman, G. (2013) Analysis of stochastic matching markets. International Journal of Game Theory, 42(4), pp. 1021-1040. (doi: 10.1007/s00182-012-0352-8)
Kwiatkowska, M., Norman, G. , Parker, D. and Qu, H. (2013) Compositional probabilistic verification through multi-objective model checking. Information and Computation, 232(6), pp. 38-65. (doi: 10.1016/j.ic.2013.10.001)
2012
Julvez, J., Kwiatkowska, M., Norman, G. and Parker, D. (2012) Evaluation of sustained stochastic oscillations by means of a system of differential equations. International Journal of Computers and Applications, 19(2), pp. 101-111.
Di Pierro, A. and Norman, G. (Eds.) (2012) Quantitative Aspects of Programming Languages (QAPL 2010). Series: Theoretical Computer Science. Elsevier.
Duflot, M., Kwiatkowska, M., Norman, G. , Parker, D., Peyronnet, S., Picaronny, C. and Sproston, J. (2012) Practical applications of probabilistic model checking to communication protocols. In: Gnesi, S. and Margaria, T. (eds.) Formal Methods for Industrial Critical Systems: A Survey of Applications. Wiley, pp. 133-150. ISBN 9780470876183 (doi: 10.1002/9781118459898.ch7)
Kwiatkowska, M., Norman, G. and Parker, D. (2012) Probabilistic verification of Herman's self-stabilisation algorithm. Formal Aspects of Computing, 24(4-6), pp. 661-670. (doi: 10.1007/s00165-012-0227-6)
2011
Hahn, E. M., Norman, G. , Parker, D., Wachter, B. and Zhang, L. (2011) Game-based abstraction and controller synthesis for probabilistic Hybrid Systems. In: QEST 2011: 8th International Conference on Quantitative Evaluation of SysTems, Aachen, Germany, 5-8 September 2011, pp. 69-78.
Massink, M. and Norman, G. (Eds.) (2011) Proceedings 9th Workshop on Quantitative Aspects of Programming Languages (QAPL'11), Saarbrücken, Germany, 1-3 April 2011. Series: Electronic Proceedings in Theoretical Computer Science. Open Publishing Association.
Forejt, V., Kwiatkowska, M., Norman, G. and Parker, D. (2011) Automated verification techniques for probabilistic systems. In: Formal Methods for Eternal Networked Software Systems 11th International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM 2011, Bertinoro, Italy, June 13-18, 2011, pp. 53-113. (doi: 10.1007/978-3-642-21455-4_3)
Forejt, V., Kwiatkowska, M., Norman, G. , Parker, D. and Qu, H. (2011) Quantitative multi-objective verification for probabilistic systems. In: Tools and Algorithms for the Construction and Analysis of Systems (TACS 2011), Saarbrücken, Germany, 26 March - 3 April 2011, pp. 112-127. (doi: 10.1007/978-3-642-19835-9_11)
Júlvez, J., Kwiatkowska, M., Norman, G. and Parker, D. (2011) A systematic approach to evaluate sustained stochastic oscillations. In: ISCA 3rd International Conference on Bioinformatics and Computational Biology (BICoB'11), Monte Carlo Resort, Las Vegas, Nevada, USA, July 18-21, 2011,
Kwiatkowska, M., Norman, G. and Parker, D. (2011) PRISM 4.0: verification of probabilistic real-time systems. Lecture Notes in Computer Science, 6806, pp. 585-591. (doi: 10.1007/978-3-642-22110-1_47)
Kwiatkowska, M., Norman, G. and Parker, D. (2011) Probabilistic model checking for systems biology. In: Iyengar, M.S. (ed.) Symbolic Systems Biology: Theory and Methods. Jones and Bartlett: Sudbury, Mass., USA. ISBN 9780763753702
2010
Kattenbelt, M., Kwiatkowska, M., Norman, G. and Parker, D. (2010) A game-based abstraction-refinement framework for Markov decision processes. Formal Methods in System Design, 36(3), pp. 246-280. (doi: 10.1007/s10703-010-0097-6)
Di Pierro, A. and Norman, G. (Eds.) (2010) Proceedings 8th Workshop on Quantitative Aspects of Programming Languages (QAPL'10). Series: Electronic Proceedings in Theoretical Computer Science (EPTCS). EPTCS.
Forejt, V., Kwiatkowska, M., Norman, G. and Trivedi, A. (2010) Expected reachability-time games. Lecture Notes in Computer Science, 6246, pp. 122-136. (doi: 10.1007/978-3-642-15297-9_11)
Kwiatkowska, M., Norman, G. and Parker, D. (2010) Advances and challenges of probabilistic model checking. In: Proceedings. 48th Annual Allerton Conference on Communication, Control and Computing, Allerton Retreat Center, Monticello, Illinois, September 29 – October 1, 2010, (Unpublished)
Kwiatkowska, M., Norman, G. and Parker, D. (2010) A framework for verification of software with time and probabilities. Lecture Notes in Computer Science, 6246, pp. 25-45. (doi: 10.1007/978-3-642-15297-9_4)
Kwiatkowska, M., Norman, G. , Parker, D. and Qu, U. (2010) Assume-guarantee verification for probabilistic systems. In: Esparza, J. and Majumdar, R. (eds.) Tools and algorithms for the construction and analysis of systems : 16th international conference, TACAS 2010, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010 : proceedings. Series: Lecture Notes in Computer Science, 6015. Springer. ISBN 9783642120015
2009
Chatzikokolakis, K., Norman, G. and Parker, D. (2009) Bisimulation for demonic schedulers. In: De Alfaro, L. (ed.) Foundations of Software Science and Computational Structures: 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings. Series: Lecture notes in computer science (5504). Springer, pp. 318-332. ISBN 9783642005961 (doi: 10.1007/978-3-642-00596-1_23)
Jurdziński, M., Kwiatkowska, M., Norman, G. and Trivedi, A. (2009) Concavely-priced probabilistic timed automata. In: CONCUR 2009 - Concurrency Theory: 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings. Series: Lecture notes in computer science (5710). Springer, pp. 415-430. ISBN 9783642040801 (doi: 10.1007/978-3-642-04081-8_28)
Kattenbelt, M., Kwiatkowska, M., Norman, G. and Parker, D. (2009) Abstraction refinement for probabilistic software. In: Jones, N.D. and Müller-Olm, M. (eds.) Verification, Model Checking, And Abstract Interpretation 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009 : Proceedings. Series: Lecture notes in computer science (5403). Springer, pp. 182-197. ISBN 9783540939009 (doi: 10.1007/978-3-540-93900-9)
Kwiatkowska, M., Norman, G. and Parker, D. (2009) PRISM: Probabilistic model checking for performance and reliability analysis. ACM SIGMETRICS Performance Evaluation Review, 36(4), pp. 40-45. (doi: 10.1145/1530873.1530882)
Kwiatkowska, M., Norman, G. and Parker, D. (2009) Quantitative verification techniques for biological processes. In: Condon, A., Harel, D., Kok, J.N., Salomaa, A. and Winfree, E. (eds.) Algorithmic Bioprocesses. Series: Natural computing series. Springer, pp. 391-409. ISBN 9783540888697 (doi: 10.1007/978-3-540-88869-7)
Kwiatkowska, M., Norman, G. and Parker, D. (2009) Stochastic games for verification of probabilistic timed automata. In: Formal Modeling and Analysis of Timed Systems: 7th International Conference, FORMATS 2009, Budapest, Hungary, September 14-16, 2009. Proceedings. Series: Lecture Notes in Computer Science, (5813). Springer, pp. 212-227. ISBN 9783642043673 (doi: 10.1007/978-3-642-04368-0_17)
Kwiatkowska, M., Norman, G. , Parker, D. and Vigliotti, M.G. (2009) Probabilistic mobile ambients. Theoretical Computer Science, 410(12-13), pp. 1272-1303. (doi: 10.1016/j.tcs.2008.12.058)
Norman, G. , Palamidessi, C., Parker, D. and Wu, P. (2009) Model checking probabilistic and stochastic extensions of the pi-calculus. IEEE Transactions on Software Engineering, 35(2-3), pp. 209-223. (doi: 10.1109/TSE.2008.77)
2008
Heath, J., Kwiatkowska, M., Norman, G. , Parker, D. and Tymchyshyn, O. (2008) Probabilistic model checking of complex biological pathways. Theoretical Computer Science, 391(3), pp. 239-257. (doi: 10.1016/j.tcs.2007.11.013)
Kattenbelt, M., Kwiatkowska, M., Norman, G. and Parker, D. (2008) Game-based probabilistic predicate abstraction in PRISM. Electronic Notes in Theoretical Computer Science, 220(3), pp. 5-21. (doi: 10.1016/j.entcs.2008.11.016)
Kwiatkowska, M., Norman, G. and Parker, D. (2008) Analysis of a gossip protocol in PRISM. ACM SIGMETRICS Performance Evaluation Review, 36(3), pp. 17-22. (doi: 10.1145/1481506.1481511)
Kwiatkowska, M., Norman, G. and Parker, D. (2008) Using probabilistic model checking in systems biology. ACM SIGMETRICS Performance Evaluation Review, 34(4), pp. 14-21. (doi: 10.1145/1364644.1364651)
Kwiatkowska, M., Norman, G. , Parker, D. and Sproston, J. (2008) Verification of real-time probabilistic systems. In: Merz, S. and Navet, N. (eds.) Modeling and Verification of Real-Time Systems: Formalisms and Software Tools. John Wiley & Sons Ltd., pp. 249-288. ISBN 9781848210134
Roy, P., Parker, D., Norman, G. and de Alfaro, L. (2008) Symbolic Magnifying Lens Abstraction in Markov Decision Processes. In: International Conference on Quantitative Evaluation of Systems (QEST'08), St. Malo, France, 14-17 Sept. 2008, pp. 103-112. (doi: 10.1109/QEST.2008.41)
2007
Kwiatkowska, M., Norman, G. and Parker, D. (2007) Controller dependability analysis by probabilistic model checking. Control Engineering Practice, 15(11), pp. 1427-1434. (doi: 10.1016/j.conengprac.2006.07.003)
Kwiatkowska, M., Norman, G. and Parker, D. (2007) Stochastic model checking. In: Bernardo, M. and Hillston, J. (eds.) Formal Methods for Performance Evaluation: 7th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2007, Bertinoro, Italy, May 28-June 2, 2007, Advanced Lectures. Series: Lecture notes in computer science (4486). Springer, pp. 220-270. ISBN 9783540725220 (doi: 10.1007/978-3-540-72522-0_6)
Kwiatkowska, M., Norman, G. , Sproston, J. and Wang, F. (2007) Symbolic model checking for probabilistic timed automata. Information and Computation, 205(7), pp. 1027-1077. (doi: 10.1016/j.ic.2007.01.004)
Norman, G. , Palamidessi, C., Parker, D. and Wu, P. (2007) Model checking the probabilistic pi-calculus. In: Proceedings Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007), Edinburgh, Scotland, September 17-19, 2007, pp. 169-178. (doi: 10.1109/QEST.2007.31)
2006
Duflot, M., Kwiatkowska, M., Norman, G. and Parker, D. (2006) A formal analysis of bluetooth device discovery. International Journal on Software Tools for Technology Transfer (STTT), 8(6), pp. 621-632. (doi: 10.1007/s10009-006-0014-x)
Norman, G. and Shmatikov, V. (2006) Analysis of probabilistic contract signing. Journal of Computer Security, 14(6), pp. 561-589.
Heath, J., Kwiatkowska, M., Norman, G. , Parker, D. and Tymchyshyn, O. (2006) Probabilistic model checking of complex biological pathways. In: Computational Methods in Systems Biology (CMSB'06), Trento, Italy, October 18-19, 2006, pp. 32-47.
Kwiatkowska, M., Norman, G. , Parker, D. and Sproston, J. (2006) Performance analysis of probabilistic timed automata using digital clocks. Formal Methods in System Design, 29(1), pp. 33-78. (doi: 10.1007/s10703-006-0005-2)
Younes, H.L.S., Kwiatkowska, M., Norman, G. and Parker, D. (2006) Numerical vs. statistical probabilistic model checking. International Journal on Software Tools for Technology Transfer (STTT), 8(3), pp. 216-228. (doi: 10.1007/s10009-005-0187-8)
Hinton, A., Kwiatkowska, M., Parker, D. and Norman, G. (2006) PRISM: a tool for automatic verification of probabilistic systems. Lecture Notes in Computer Science, 3920, pp. 441-444. (doi: 10.1007/11691372_29)
Kwiatkowska, M., Norman, G. and Pacheco, A. (2006) Model checking expected time and expected reward formulae with random time bounds. Computers and Mathematics with Applications, 51(2), pp. 305-316. (doi: 10.1016/j.camwa.2005.11.016)
Groesser, M., Norman, G. , Baier, C., Ciesinski, F., Kwiatkowska, M. and Parker, D. (2006) On reduction criteria for probabilistic reward models. In: Arun-Kumar, S. and Garg, N. (eds.) Foundations of Software Technology and Theoretical Computer Science (FSTTCS'06). Series: Lecture notes in computer science (4337). Springer Verlag, pp. 309-320. ISBN 9783540499954 (doi: 10.1007/11944836_29)
Kwiatkowska, M., Norman, G. and Parker, D. (2006) Game-based abstraction for Markov decision processes. In: 3rd International Conference on Quantitative Evaluation of Systems (QEST'06), Riverside, California, USA, 11-14 Sept 2006, pp. 157-166. (doi: 10.1109/QEST.2006.19)
Kwiatkowska, M., Norman, G. and Parker, D. (2006) Symmetry reduction for probabilistic model checking. Lecture Notes in Computer Science, 4144, pp. 234-248. (doi: 10.1007/11817963_23)
Kwiatkowska, M., Norman, G. , Parker, D., Tymchyshyn, O., Heath, J. and Gaffney, E. (2006) Simulation and verification for computational modelling of signalling pathways. In: Perrone, L., Wieland, F.P., Liu, J., Lawson, B.J., Nicol, D.M. and Fujimoto, R.M. (eds.) Proceedings of the 2006 Winter Simulation Conference. WSC, pp. 1666-1674. ISBN 1424405009 (doi: 10.1109/WSC.2006.323029)
2005
Norman, G. , Parker, P., Kwiatkowska, M. and Shukla, S. (2005) Evaluating the reliability of NAND multiplexing with PRISM. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 24(10), 1629 -1637. (doi: 10.1109/TCAD.2005.852033)
Kwiatkowska, M., Norman, G. and Parker, D. (2005) Probabilistic Model Checking and Power-Aware Computing. In: 7th International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS), Torino, Italy, September 23-24, 2005, pp. 6-9.
Norman, G. , Parker, D., Kwiatkowska, M., Shukla, S. and Gupta, R. (2005) Using probabilistic model checking for dynamic power management. Formal Aspects of Computing, 17(2), pp. 160-176. (doi: 10.1007/s00165-005-0062-0)
2004
Daws, C., Kwiatkowska, M. and Norman, G. (2004) Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM. International Journal on Software Tools for Technology Transfer (STTT), 5(2), pp. 221-236. (doi: 10.1007/s10009-003-0118-5)
Kwiatkowska, M., Norman, G. and Parker, D. (2004) Probabilistic symbolic model checking with PRISM: a hybrid approach. International Journal on Software Tools for Technology Transfer (STTT), 6(2), pp. 128-142. (doi: 10.1007/s10009-004-0140-2)
2002
Kwiatkowska, M., Norman, G. , Segala, R. and Sproston, J. (2002) Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science, 282(1), pp. 101-150. (doi: 10.1016/S0304-3975(01)00046-9)
2001
Katoen, J.P., Kwiatkowska, M., Norman, G. and Parker, D. (2001) Faster and symbolic CTMC model checking. In: de Alfaro, L. and Gilmore, S. (eds.) Process Algebra and Probabilistic Methods : Performance Modeling and Verification : Joint International Workshop. Series: Lecture notes in computer science (2165). Springer-Verlag: Berlin; New York, pp. 23-38. ISBN 9783540425564 (doi: 10.1007/3-540-44804-7_2)
Kwiatkowska, M., Norman, G. and Segala, R. (2001) Automated verication of a randomized distributed concensus protocol using Cadence SMV and PRISM. In: Berry, G., Common, H. and Finkel, A. (eds.) Computer Aided Verification: 13th International Conference, CAV 2001, Paris, France, July 2001 : Proceedings. Series: Lecture notes in computer science (2102). Springer-Verlag: Berlin, pp. 194-206. ISBN 9783540423454 (doi: 10.1007/3-540-44585-4_17)
Articles
Yan, R., Santos, G., Norman, G. , Parker, D. and Kwiatkowska, M. (2024) Strategy synthesis for zero-sum neuro-symbolic concurrent stochastic games. Information and Computation, 300, 105193. (doi: 10.1016/j.ic.2024.105193) (Accepted for Publication)
Kavanagh, W., Fraser, D., Hunter, E. , Pancheva, A., Parkinson, J. , Paun, I., Wallis, T. , Ada, M. B., Border, H. and Norman, G. (2022) Experience report: challenges and opportunities of remote labs for a computer science department. Postgraduate Pedagogies, 2(1), pp. 173-207.
Kwiatkowska, M., Norman, G. and Parker, D. (2022) Probabilistic model checking and autonomy. Annual Review of Control, Robotics, and Autonomous Systems, 5, (doi: 10.1146/annurev-control-042820-010947)
Kwiatkowska, M., Norman, G. , Parker, D. and Santos, G. (2021) Automatic verification of concurrent stochastic systems. Formal Methods in System Design, 58(1-2), pp. 188-250. (doi: 10.1007/s10703-020-00356-y)
Kavanagh, W. , Miller, A. , Norman, G. and Andrei, O. (2021) Balancing turn-based games with chained strategy generation. IEEE Transactions on Games, 13(2), pp. 113-122. (doi: 10.1109/TG.2019.2943227)
Fraser, D., Giaquinta, R., Hoffmann, R., Ireland, M., Miller, A. and Norman, G. (2020) Collaborative models for autonomous systems controller synthesis. Formal Aspects of Computing, 32, pp. 157-186. (doi: 10.1007/s00165-020-00508-1)
Scott, P. H., Veitch, N. J. , Gadegaard, H., Mughal, M., Norman, G. and Welsh, M. (2018) Enhancing theoretical understanding of a practical biology course using active and self-directed learning strategies. Journal of Biological Education, 52(2), pp. 184-195. (doi: 10.1080/00219266.2017.1293557)
Norman, G. , Parker, D. and Zou, X. (2017) Verification and control of partially observable probabilistic systems. Real-Time Systems, 53(3), pp. 354-402. (doi: 10.1007/s11241-017-9269-4)
Jovanovic, A., Kwiatkowska, M., Norman, G. and Peyras, Q. (2017) Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata. Theoretical Computer Science, 669, pp. 1-21. (doi: 10.1016/j.tcs.2017.01.015)
Forejt, V., Kwiatkowska, M., Norman, G. and Trivedi, A. (2016) Expected reachability-time games. Theoretical Computer Science, 631, pp. 139-160. (doi: 10.1016/j.tcs.2016.04.021)
Hoffmann, R., Ireland, M. , Miller, A. , Norman, G. and Veres, S. (2016) Autonomous agent behaviour modelled in PRISM: a case study. Lecture Notes in Computer Science, 9641, pp. 104-110. (doi: 10.1007/978-3-319-32582-8_7)
Jovanovic, A., Norman, G. and Kwiatkowska, M. (2015) Symbolic Minimum Expected Time Controller Synthesis for Probabilistic Timed Automata. Lecture Notes in Computer Science, 9268, pp. 140-155. (doi: 10.1007/978-3-319-22975-1_10)
Norman, G. , Parker, D. and Zou, X. (2015) Verification and Control of Partially Observable Probabilistic Real-Time Systems. Lecture Notes in Computer Science, 9268, pp. 240-255. (doi: 10.1007/978-3-319-22975-1_16)
Abate, A., Kwiatkowska, M., Norman, G. and Parker, D. (2014) Probabilistic model checking of labelled Markov processes via finite approximate bisimulations. Lecture Notes in Computer Science, 8464, pp. 40-58. (doi: 10.1007/978-3-319-06880-0_2)
Biro, P. and Norman, G. (2013) Analysis of stochastic matching markets. International Journal of Game Theory, 42(4), pp. 1021-1040. (doi: 10.1007/s00182-012-0352-8)
Kwiatkowska, M., Norman, G. , Parker, D. and Qu, H. (2013) Compositional probabilistic verification through multi-objective model checking. Information and Computation, 232(6), pp. 38-65. (doi: 10.1016/j.ic.2013.10.001)
Julvez, J., Kwiatkowska, M., Norman, G. and Parker, D. (2012) Evaluation of sustained stochastic oscillations by means of a system of differential equations. International Journal of Computers and Applications, 19(2), pp. 101-111.
Kwiatkowska, M., Norman, G. and Parker, D. (2012) Probabilistic verification of Herman's self-stabilisation algorithm. Formal Aspects of Computing, 24(4-6), pp. 661-670. (doi: 10.1007/s00165-012-0227-6)
Kwiatkowska, M., Norman, G. and Parker, D. (2011) PRISM 4.0: verification of probabilistic real-time systems. Lecture Notes in Computer Science, 6806, pp. 585-591. (doi: 10.1007/978-3-642-22110-1_47)
Kattenbelt, M., Kwiatkowska, M., Norman, G. and Parker, D. (2010) A game-based abstraction-refinement framework for Markov decision processes. Formal Methods in System Design, 36(3), pp. 246-280. (doi: 10.1007/s10703-010-0097-6)
Forejt, V., Kwiatkowska, M., Norman, G. and Trivedi, A. (2010) Expected reachability-time games. Lecture Notes in Computer Science, 6246, pp. 122-136. (doi: 10.1007/978-3-642-15297-9_11)
Kwiatkowska, M., Norman, G. and Parker, D. (2010) A framework for verification of software with time and probabilities. Lecture Notes in Computer Science, 6246, pp. 25-45. (doi: 10.1007/978-3-642-15297-9_4)
Kwiatkowska, M., Norman, G. and Parker, D. (2009) PRISM: Probabilistic model checking for performance and reliability analysis. ACM SIGMETRICS Performance Evaluation Review, 36(4), pp. 40-45. (doi: 10.1145/1530873.1530882)
Kwiatkowska, M., Norman, G. , Parker, D. and Vigliotti, M.G. (2009) Probabilistic mobile ambients. Theoretical Computer Science, 410(12-13), pp. 1272-1303. (doi: 10.1016/j.tcs.2008.12.058)
Norman, G. , Palamidessi, C., Parker, D. and Wu, P. (2009) Model checking probabilistic and stochastic extensions of the pi-calculus. IEEE Transactions on Software Engineering, 35(2-3), pp. 209-223. (doi: 10.1109/TSE.2008.77)
Heath, J., Kwiatkowska, M., Norman, G. , Parker, D. and Tymchyshyn, O. (2008) Probabilistic model checking of complex biological pathways. Theoretical Computer Science, 391(3), pp. 239-257. (doi: 10.1016/j.tcs.2007.11.013)
Kattenbelt, M., Kwiatkowska, M., Norman, G. and Parker, D. (2008) Game-based probabilistic predicate abstraction in PRISM. Electronic Notes in Theoretical Computer Science, 220(3), pp. 5-21. (doi: 10.1016/j.entcs.2008.11.016)
Kwiatkowska, M., Norman, G. and Parker, D. (2008) Analysis of a gossip protocol in PRISM. ACM SIGMETRICS Performance Evaluation Review, 36(3), pp. 17-22. (doi: 10.1145/1481506.1481511)
Kwiatkowska, M., Norman, G. and Parker, D. (2008) Using probabilistic model checking in systems biology. ACM SIGMETRICS Performance Evaluation Review, 34(4), pp. 14-21. (doi: 10.1145/1364644.1364651)
Kwiatkowska, M., Norman, G. and Parker, D. (2007) Controller dependability analysis by probabilistic model checking. Control Engineering Practice, 15(11), pp. 1427-1434. (doi: 10.1016/j.conengprac.2006.07.003)
Kwiatkowska, M., Norman, G. , Sproston, J. and Wang, F. (2007) Symbolic model checking for probabilistic timed automata. Information and Computation, 205(7), pp. 1027-1077. (doi: 10.1016/j.ic.2007.01.004)
Duflot, M., Kwiatkowska, M., Norman, G. and Parker, D. (2006) A formal analysis of bluetooth device discovery. International Journal on Software Tools for Technology Transfer (STTT), 8(6), pp. 621-632. (doi: 10.1007/s10009-006-0014-x)
Norman, G. and Shmatikov, V. (2006) Analysis of probabilistic contract signing. Journal of Computer Security, 14(6), pp. 561-589.
Kwiatkowska, M., Norman, G. , Parker, D. and Sproston, J. (2006) Performance analysis of probabilistic timed automata using digital clocks. Formal Methods in System Design, 29(1), pp. 33-78. (doi: 10.1007/s10703-006-0005-2)
Younes, H.L.S., Kwiatkowska, M., Norman, G. and Parker, D. (2006) Numerical vs. statistical probabilistic model checking. International Journal on Software Tools for Technology Transfer (STTT), 8(3), pp. 216-228. (doi: 10.1007/s10009-005-0187-8)
Hinton, A., Kwiatkowska, M., Parker, D. and Norman, G. (2006) PRISM: a tool for automatic verification of probabilistic systems. Lecture Notes in Computer Science, 3920, pp. 441-444. (doi: 10.1007/11691372_29)
Kwiatkowska, M., Norman, G. and Pacheco, A. (2006) Model checking expected time and expected reward formulae with random time bounds. Computers and Mathematics with Applications, 51(2), pp. 305-316. (doi: 10.1016/j.camwa.2005.11.016)
Kwiatkowska, M., Norman, G. and Parker, D. (2006) Symmetry reduction for probabilistic model checking. Lecture Notes in Computer Science, 4144, pp. 234-248. (doi: 10.1007/11817963_23)
Norman, G. , Parker, P., Kwiatkowska, M. and Shukla, S. (2005) Evaluating the reliability of NAND multiplexing with PRISM. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 24(10), 1629 -1637. (doi: 10.1109/TCAD.2005.852033)
Norman, G. , Parker, D., Kwiatkowska, M., Shukla, S. and Gupta, R. (2005) Using probabilistic model checking for dynamic power management. Formal Aspects of Computing, 17(2), pp. 160-176. (doi: 10.1007/s00165-005-0062-0)
Daws, C., Kwiatkowska, M. and Norman, G. (2004) Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM. International Journal on Software Tools for Technology Transfer (STTT), 5(2), pp. 221-236. (doi: 10.1007/s10009-003-0118-5)
Kwiatkowska, M., Norman, G. and Parker, D. (2004) Probabilistic symbolic model checking with PRISM: a hybrid approach. International Journal on Software Tools for Technology Transfer (STTT), 6(2), pp. 128-142. (doi: 10.1007/s10009-004-0140-2)
Kwiatkowska, M., Norman, G. , Segala, R. and Sproston, J. (2002) Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science, 282(1), pp. 101-150. (doi: 10.1016/S0304-3975(01)00046-9)
Books
Norman, G. and William, S. eds. (2014) Quantitative Evaluation of Systems: 11th International Conference, Florence, Italy, 8-10 September 2014. Series: Lecture Notes in Computer Science, 8657. Springer Verlag. ISBN 9783319106960
Book Sections
Kwiatkowska, M., Norman, G. , Parker, D. and Santos, G. (2022) Symbolic verification and strategy synthesis for turn-based stochastic games. In: Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday. Series: Lecture Notes In Computer 13660. Springer. (Accepted for Publication)
Kwiatkowska, M., Norman, G. and Parker, D. (2019) Verification and Control of Turn-Based Probabilistic Real-Time Games. In: Alvim, M. S., Chatzikokolakis, K., Olarte, C. and Valencia, F. (eds.) The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy: Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday. Series: Lecture notes in computer science (11760). Springer: Cham, pp. 379-396. ISBN 9783030311742 (doi: 10.1007/978-3-030-31175-9_22)
Kwiatkowska, M., Norman, G. , Parker, D. and Santos, G. (2019) Equilibria-based probabilistic model checking for concurrent stochastic games. In: ter Beek, M. H., McIver, A. and Oliveira, J. N. (eds.) Formal Methods - The Next 30 Years. Series: Lecture Notes in Computer Science (11800). Springer, pp. 298-315. ISBN 9783030309411 (doi: 10.1007/978-3-030-30942-8_19)
Kwiatkowska, M., Norman, G. and Parker, D. (2017) Probabilistic model checking: advances and applications. In: Drechsler, R. (ed.) Formal System Verification: State-of the-Art and Future Trends. Springer Verlag, pp. 73-121. ISBN 9783319576831 (doi: 10.1007/978-3-319-57685-5_3)
Ferdous, M. S., Norman, G. , Jøsang, A. and Poet, R. (2015) Mathematical modelling of trust issues in federated identity management. In: Damsgaard Jensen, C., Marsh, S., Dimitrakos, T. and Murayama, Y. (eds.) Trust Management IX: 9th Ifip Wg 11.11 International Conference, Ifiptm 2015, Hamburg, Germany, May 26-28, 2015, Proceedings. Series: IFIP Advances in Information and Communication Technology (454). Springer International Publishing, pp. 13-29. ISBN 9783319184906 (doi: 10.1007/978-3-319-18491-3_2)
Duflot, M., Kwiatkowska, M., Norman, G. , Parker, D., Peyronnet, S., Picaronny, C. and Sproston, J. (2012) Practical applications of probabilistic model checking to communication protocols. In: Gnesi, S. and Margaria, T. (eds.) Formal Methods for Industrial Critical Systems: A Survey of Applications. Wiley, pp. 133-150. ISBN 9780470876183 (doi: 10.1002/9781118459898.ch7)
Kwiatkowska, M., Norman, G. and Parker, D. (2011) Probabilistic model checking for systems biology. In: Iyengar, M.S. (ed.) Symbolic Systems Biology: Theory and Methods. Jones and Bartlett: Sudbury, Mass., USA. ISBN 9780763753702
Kwiatkowska, M., Norman, G. , Parker, D. and Qu, U. (2010) Assume-guarantee verification for probabilistic systems. In: Esparza, J. and Majumdar, R. (eds.) Tools and algorithms for the construction and analysis of systems : 16th international conference, TACAS 2010, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010 : proceedings. Series: Lecture Notes in Computer Science, 6015. Springer. ISBN 9783642120015
Chatzikokolakis, K., Norman, G. and Parker, D. (2009) Bisimulation for demonic schedulers. In: De Alfaro, L. (ed.) Foundations of Software Science and Computational Structures: 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings. Series: Lecture notes in computer science (5504). Springer, pp. 318-332. ISBN 9783642005961 (doi: 10.1007/978-3-642-00596-1_23)
Jurdziński, M., Kwiatkowska, M., Norman, G. and Trivedi, A. (2009) Concavely-priced probabilistic timed automata. In: CONCUR 2009 - Concurrency Theory: 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings. Series: Lecture notes in computer science (5710). Springer, pp. 415-430. ISBN 9783642040801 (doi: 10.1007/978-3-642-04081-8_28)
Kattenbelt, M., Kwiatkowska, M., Norman, G. and Parker, D. (2009) Abstraction refinement for probabilistic software. In: Jones, N.D. and Müller-Olm, M. (eds.) Verification, Model Checking, And Abstract Interpretation 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009 : Proceedings. Series: Lecture notes in computer science (5403). Springer, pp. 182-197. ISBN 9783540939009 (doi: 10.1007/978-3-540-93900-9)
Kwiatkowska, M., Norman, G. and Parker, D. (2009) Quantitative verification techniques for biological processes. In: Condon, A., Harel, D., Kok, J.N., Salomaa, A. and Winfree, E. (eds.) Algorithmic Bioprocesses. Series: Natural computing series. Springer, pp. 391-409. ISBN 9783540888697 (doi: 10.1007/978-3-540-88869-7)
Kwiatkowska, M., Norman, G. and Parker, D. (2009) Stochastic games for verification of probabilistic timed automata. In: Formal Modeling and Analysis of Timed Systems: 7th International Conference, FORMATS 2009, Budapest, Hungary, September 14-16, 2009. Proceedings. Series: Lecture Notes in Computer Science, (5813). Springer, pp. 212-227. ISBN 9783642043673 (doi: 10.1007/978-3-642-04368-0_17)
Kwiatkowska, M., Norman, G. , Parker, D. and Sproston, J. (2008) Verification of real-time probabilistic systems. In: Merz, S. and Navet, N. (eds.) Modeling and Verification of Real-Time Systems: Formalisms and Software Tools. John Wiley & Sons Ltd., pp. 249-288. ISBN 9781848210134
Kwiatkowska, M., Norman, G. and Parker, D. (2007) Stochastic model checking. In: Bernardo, M. and Hillston, J. (eds.) Formal Methods for Performance Evaluation: 7th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2007, Bertinoro, Italy, May 28-June 2, 2007, Advanced Lectures. Series: Lecture notes in computer science (4486). Springer, pp. 220-270. ISBN 9783540725220 (doi: 10.1007/978-3-540-72522-0_6)
Groesser, M., Norman, G. , Baier, C., Ciesinski, F., Kwiatkowska, M. and Parker, D. (2006) On reduction criteria for probabilistic reward models. In: Arun-Kumar, S. and Garg, N. (eds.) Foundations of Software Technology and Theoretical Computer Science (FSTTCS'06). Series: Lecture notes in computer science (4337). Springer Verlag, pp. 309-320. ISBN 9783540499954 (doi: 10.1007/11944836_29)
Kwiatkowska, M., Norman, G. , Parker, D., Tymchyshyn, O., Heath, J. and Gaffney, E. (2006) Simulation and verification for computational modelling of signalling pathways. In: Perrone, L., Wieland, F.P., Liu, J., Lawson, B.J., Nicol, D.M. and Fujimoto, R.M. (eds.) Proceedings of the 2006 Winter Simulation Conference. WSC, pp. 1666-1674. ISBN 1424405009 (doi: 10.1109/WSC.2006.323029)
Katoen, J.P., Kwiatkowska, M., Norman, G. and Parker, D. (2001) Faster and symbolic CTMC model checking. In: de Alfaro, L. and Gilmore, S. (eds.) Process Algebra and Probabilistic Methods : Performance Modeling and Verification : Joint International Workshop. Series: Lecture notes in computer science (2165). Springer-Verlag: Berlin; New York, pp. 23-38. ISBN 9783540425564 (doi: 10.1007/3-540-44804-7_2)
Kwiatkowska, M., Norman, G. and Segala, R. (2001) Automated verication of a randomized distributed concensus protocol using Cadence SMV and PRISM. In: Berry, G., Common, H. and Finkel, A. (eds.) Computer Aided Verification: 13th International Conference, CAV 2001, Paris, France, July 2001 : Proceedings. Series: Lecture notes in computer science (2102). Springer-Verlag: Berlin, pp. 194-206. ISBN 9783540423454 (doi: 10.1007/3-540-44585-4_17)
Edited Books
Di Pierro, A. and Norman, G. (Eds.) (2012) Quantitative Aspects of Programming Languages (QAPL 2010). Series: Theoretical Computer Science. Elsevier.
Massink, M. and Norman, G. (Eds.) (2011) Proceedings 9th Workshop on Quantitative Aspects of Programming Languages (QAPL'11), Saarbrücken, Germany, 1-3 April 2011. Series: Electronic Proceedings in Theoretical Computer Science. Open Publishing Association.
Di Pierro, A. and Norman, G. (Eds.) (2010) Proceedings 8th Workshop on Quantitative Aspects of Programming Languages (QAPL'10). Series: Electronic Proceedings in Theoretical Computer Science (EPTCS). EPTCS.
Research Reports or Papers
Norman, G. and Parker, D. (2014) Quantitative Verification: Formal Guarantees for Timeliness, Reliability and Performance. Technical Report. London Mathematical Society and Smith Institute.
Conference Proceedings
Yan, R., Santos, G., Norman, G. , Parker, D. and Kwiatkowska, M. (2024) Partially Observable Stochastic Games with Neural Perception Mechanisms. In: 26th International Symposium on Formal Methods (FM24), Milan, Italy, 11-13 September 2024, (Accepted for Publication)
Yan, R., Santos, G., Norman, G. , Parker, D. and Kwiatkowska, M. (2024) HSVI-based Online Minimax Strategies for Partially Observable Stochastic Games with Neural Perception Mechanisms. In: 2024 Learning for Dynamics and Control Conference (L4DC), Oxford, UK, 15-17 July, 2024, (Accepted for Publication)
Kwiatkowska, M., Norman, G. , Parker, D., Santos, G. and Yang, R. (2022) Probabilistic Model Checking for Strategic Equilibria-based Decision Making: Advances and Challenges. In: 47th International Symposium on Mathematical Foundations of Computer Science, Vienna, Austria, 22-26 Aug 2022, p. 4. ISBN 9783959772563 (doi: 10.4230/LIPIcs.MFCS.2022.4)
Kwiatkowska, M., Norman, G. , Parker, D. and Santos, G. (2022) Correlated Equilibria and Fairness in Concurrent Stochastic Games. In: 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'22), Munich, Germany, 02-07 Apr 2022, pp. 60-78. ISBN 978-3-030-99527-0 (doi: 10.1007/978-3-030-99527-0_4)
Kwiatkowska, M., Norman, G. , Parker, D. and Santos, G. (2020) Multi-player Equilibria Verification for Concurrent Stochastic Games. In: 17th International Conference on Quantitative Evaluation of SysTems (QEST 2020), 31 Aug - 03 Sep 2020, ISBN 9783030598532 (doi: 10.1007/978-3-030-59854-9_7)
Kwiatkowska, M., Norman, G. , Parker, D. and Santos, G. (2018) Automated verification of concurrent stochastic games. In: 15th International Conference on Quantitative Evaluation of SysTems (QEST 2018), Beijing, China, 04-07 Sept 2018, pp. 223-239. ISBN 9783319991535 (doi: 10.1007/978-3-319-99154-2_14)
Giaquinta, R., Hoffmann, R., Ireland, M. , Miller, A. and Norman, G. (2018) Strategy Synthesis for Autonomous Agents Using PRISM. In: 10th NASA Formal Methods Symposium (NFM 2018), Newport News, VA, USA, 17-19 Apr 2018, pp. 220-236. ISBN 9783319779348 (doi: 10.1007/978-3-319-77935-5_16)
Kwiatkowska, M., Norman, G. and Parker, D. (2017) Symbolic Verification and Strategy Synthesis for Linearly-Priced Probabilistic Timed Automata. In: KiMfest: A Conference in Honour of Kim G. Larsen on the Occasion of his 60th Birthday, Aalborg University, Denmark, 19-20 Aug 2017, pp. 289-309. ISBN 9783319631202 (doi: 10.1007/978-3-319-63121-9_15)
Hahn, E. M., Norman, G. , Parker, D., Wachter, B. and Zhang, L. (2011) Game-based abstraction and controller synthesis for probabilistic Hybrid Systems. In: QEST 2011: 8th International Conference on Quantitative Evaluation of SysTems, Aachen, Germany, 5-8 September 2011, pp. 69-78.
Forejt, V., Kwiatkowska, M., Norman, G. and Parker, D. (2011) Automated verification techniques for probabilistic systems. In: Formal Methods for Eternal Networked Software Systems 11th International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM 2011, Bertinoro, Italy, June 13-18, 2011, pp. 53-113. (doi: 10.1007/978-3-642-21455-4_3)
Forejt, V., Kwiatkowska, M., Norman, G. , Parker, D. and Qu, H. (2011) Quantitative multi-objective verification for probabilistic systems. In: Tools and Algorithms for the Construction and Analysis of Systems (TACS 2011), Saarbrücken, Germany, 26 March - 3 April 2011, pp. 112-127. (doi: 10.1007/978-3-642-19835-9_11)
Júlvez, J., Kwiatkowska, M., Norman, G. and Parker, D. (2011) A systematic approach to evaluate sustained stochastic oscillations. In: ISCA 3rd International Conference on Bioinformatics and Computational Biology (BICoB'11), Monte Carlo Resort, Las Vegas, Nevada, USA, July 18-21, 2011,
Kwiatkowska, M., Norman, G. and Parker, D. (2010) Advances and challenges of probabilistic model checking. In: Proceedings. 48th Annual Allerton Conference on Communication, Control and Computing, Allerton Retreat Center, Monticello, Illinois, September 29 – October 1, 2010, (Unpublished)
Roy, P., Parker, D., Norman, G. and de Alfaro, L. (2008) Symbolic Magnifying Lens Abstraction in Markov Decision Processes. In: International Conference on Quantitative Evaluation of Systems (QEST'08), St. Malo, France, 14-17 Sept. 2008, pp. 103-112. (doi: 10.1109/QEST.2008.41)
Norman, G. , Palamidessi, C., Parker, D. and Wu, P. (2007) Model checking the probabilistic pi-calculus. In: Proceedings Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007), Edinburgh, Scotland, September 17-19, 2007, pp. 169-178. (doi: 10.1109/QEST.2007.31)
Heath, J., Kwiatkowska, M., Norman, G. , Parker, D. and Tymchyshyn, O. (2006) Probabilistic model checking of complex biological pathways. In: Computational Methods in Systems Biology (CMSB'06), Trento, Italy, October 18-19, 2006, pp. 32-47.
Kwiatkowska, M., Norman, G. and Parker, D. (2006) Game-based abstraction for Markov decision processes. In: 3rd International Conference on Quantitative Evaluation of Systems (QEST'06), Riverside, California, USA, 11-14 Sept 2006, pp. 157-166. (doi: 10.1109/QEST.2006.19)
Kwiatkowska, M., Norman, G. and Parker, D. (2005) Probabilistic Model Checking and Power-Aware Computing. In: 7th International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS), Torino, Italy, September 23-24, 2005, pp. 6-9.
Supervision
- Fraser, Douglas
Applications of Model Checking in the Context of Security for Digital Twins
Teaching
I coordinate the following two undergraduate courses:
- Algorithmic Foundations 2 COMPSCI2003
- Algorithmics I (H) COMPSCI4009