2024
A Framework for Simultaneous Task Allocation and Planning under Uncertainty.
ACM Trans. Auton. Adapt. Syst., December, 2024
Safe POMDP Online Planning Among Dynamic Agents via Adaptive Conformal Prediction.
IEEE Robotics Autom. Lett., November, 2024
Strategy synthesis for zero-sum neuro-symbolic concurrent stochastic games.
Inf. Comput., 2024
Learning Provably Robust Policies in Uncertain Parametric Environments.
CoRR, 2024
Tools at the Frontiers of Quantitative Verification.
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
CoRR, 2024
Learning Algorithms for Verification of Markov Decision Processes.
CoRR, 2024
Partially-Observable Security Games for Attack-Defence Analysis in Software Systems.
Proceedings of the Software Engineering and Formal Methods - 22nd International Conference, 2024
Distributional Probabilistic Model Checking.
Proceedings of the NASA Formal Methods - 16th International Symposium, 2024
HSVI-based online minimax strategies for partially observable stochastic games with neural perception mechanisms.
Proceedings of the 6th Annual Learning for Dynamics & Control Conference, 2024
Safe POMDP Online Planning via Shielding.
Proceedings of the IEEE International Conference on Robotics and Automation, 2024
Partially Observable Stochastic Games with Neural Perception Mechanisms.
Proceedings of the Formal Methods - 26th International Symposium, 2024
Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet.
Proceedings of the Principles of Verification: Cycling the Probabilistic Landscape, 2024
Expectation vs. Reality: Towards Verification of Psychological Games.
Proceedings of the Principles of Verification: Cycling the Probabilistic Landscape, 2024
Revisiting a Pioneering Concurrent Stochastic Problem: The Erlangen Mainframe.
Proceedings of the Principles of Verification: Cycling the Probabilistic Landscape, 2024
2023
The Hamiltonian Cycle and Travelling Salesperson problems with traversal-dependent edge deletion.
J. Comput. Sci., December, 2023
Artifact for: Distributional Probabilistic Model Checking.
Dataset, September, 2023
Artifact for: Distributional Probabilistic Model Checking.
Dataset, September, 2023
Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions.
J. Artif. Intell. Res., 2023
Point-based Value Iteration for Neuro-Symbolic POMDPs.
CoRR, 2023
Multi-agent Verification and Control with Probabilistic Model Checking.
Proceedings of the Quantitative Evaluation of Systems - 20th International Conference, 2023
Using Reed-Muller Codes for Classification with Rejection and Recovery.
Proceedings of the Foundations and Practice of Security - 16th International Symposium, 2023
2022
Planning for Automated Vehicles with Human Trust.
ACM Trans. Cyber Phys. Syst., 2022
Tools and algorithms for the construction and analysis of systems: a special issue for TACAS 2020.
Int. J. Softw. Tools Technol. Transf., 2022
Partially-Observable Security Games for Automating Attack-Defense Analysis.
CoRR, 2022
Probabilistic Model Checking for Strategic Equilibria-based Decision Making: Advances and Challenges.
CoRR, 2022
Probabilistic Model Checking and Autonomy.
Annu. Rev. Control. Robotics Auton. Syst., 2022
Finite-horizon equilibria for neuro-symbolic concurrent stochastic games.
Proceedings of the Uncertainty in Artificial Intelligence, 2022
Correlated Equilibria and Fairness in Concurrent Stochastic Games.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022
Robust Anytime Learning of Markov Decision Processes.
Proceedings of the Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, 2022
Verified Probabilistic Policies for Deep Reinforcement Learning.
Proceedings of the NASA Formal Methods - 14th International Symposium, 2022
Probabilistic Model Checking for Strategic Equilibria-Based Decision Making: Advances and Challenges (Invited Talk).
Proceedings of the 47th International Symposium on Mathematical Foundations of Computer Science, 2022
A Value-based Dynamic Learning Approach for Vehicle Dispatch in Ride-Sharing.
Proceedings of the IEEE/RSJ International Conference on Intelligent Robots and Systems, 2022
Multi-Objective Controller Synthesis with Uncertain Human Preferences.
Proceedings of the 13th ACM/IEEE International Conference on Cyber-Physical Systems, 2022
Symbolic Verification and Strategy Synthesis for Turn-Based Stochastic Games.
Proceedings of the Principles of Systems Design, 2022
Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise.
Proceedings of the Thirty-Sixth AAAI Conference on Artificial Intelligence, 2022
2021
Introduction to the Special Issue on QEST 2019.
ACM Trans. Model. Comput. Simul., 2021
Automatic verification of concurrent stochastic systems.
Formal Methods Syst. Des., 2021
Quantitative verification of Kalman filters.
Formal Aspects Comput., 2021
Fault diagnosis in labelled Petri nets: A Fourier-Motzkin based approach.
Autom., 2021
Vehicle Dispatch in On-Demand Ride-Sharing with Stochastic Travel Times.
Proceedings of the IEEE/RSJ International Conference on Intelligent Robots and Systems, 2021
Verifying Reinforcement Learning up to Infinity.
Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, 2021
Optimal Online Dispatch for High-Capacity Shared Autonomous Mobility-on-Demand Systems.
Proceedings of the IEEE International Conference on Robotics and Automation, 2021
2020
ATEN: And/Or tree ensemble for inferring accurate Boolean network topology and dynamics.
Bioinform., 2020
Multi-player Equilibria Verification for Concurrent Stochastic Games.
Proceedings of the Quantitative Evaluation of Systems - 17th International Conference, 2020
On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends, 2020
Probabilistic Guarantees for Safe Deep Reinforcement Learning.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2020
Quantitative Verification of Certificate Transparency Gossip Protocols.
Proceedings of the 8th IEEE Conference on Communications and Network Security, 2020
PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020
2019
Software Adaptation for an Unmanned Undersea Vehicle.
,
,
,
,
,
,
,
,
,
,
,
IEEE Softw., 2019
Probabilistic planning with formal performance guarantees for mobile service robots.
Int. J. Robotics Res., 2019
The Quantitative Verification Benchmark Set.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019
The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019
Equilibria-Based Probabilistic Model Checking for Concurrent Stochastic Games.
Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019
Quantitative Verification of Numerical Stability for Kalman Filters.
Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019
Automated Formal Analysis of Side-Channel Attacks on Probabilistic Systems.
Proceedings of the Computer Security - ESORICS 2019, 2019
Verification and Control of Turn-Based Probabilistic Real-Time Games.
Proceedings of the Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy, 2019
2018
Replicated Computational Results (RCR) Report for "ProPPA: Probabilistic Programming for Stochastic Dynamical Systems".
ACM Trans. Model. Comput. Simul., 2018
Organisation-Oriented Coarse Graining and Refinement of Stochastic Reaction Networks.
IEEE ACM Trans. Comput. Biol. Bioinform., 2018
PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives.
Int. J. Softw. Tools Technol. Transf., 2018
Performance modelling and verification of cloud-based auto-scaling policies.
Future Gener. Comput. Syst., 2018
Automated Verification of Concurrent Stochastic Games.
Proceedings of the Quantitative Evaluation of Systems - 15th International Conference, 2018
Simultaneous Task Allocation and Planning Under Uncertainty.
Proceedings of the 2018 IEEE/RSJ International Conference on Intelligent Robots and Systems, 2018
2017
Verification and control of partially observable probabilistic systems.
Real Time Syst., 2017
Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017
Symbolic Verification and Strategy Synthesis for Linearly-Priced Probabilistic Timed Automata.
Proceedings of the Models, Algorithms, Logics and Tools, 2017
Multi-Objective Policy Generation for Mobile Robots under Probabilistic Time-Bounded Guarantees.
Proceedings of the Twenty-Seventh International Conference on Automated Planning and Scheduling, 2017
2016
Synthesizing efficient systems in probabilistic environments.
Acta Informatica, 2016
PRISM-Games 2.0: A Tool for Multi-objective Strategy Synthesis for Stochastic Games.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016
Finite-Horizon Bisimulation Minimisation for Probabilistic Systems.
Proceedings of the Model Checking Software - 23rd International Symposium, 2016
Quantitative Verification and Synthesis of Attack-Defence Scenarios.
Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016
Formal Quantitative Analysis of Reaction Networks Using Chemical Organisation Theory.
Proceedings of the Computational Methods in Systems Biology, 2016
2015
Permissive Controller Synthesis for Probabilistic Systems.
Log. Methods Comput. Sci., 2015
Optimal Policy Generation for Partially Satisfiable Co-Safe LTL Specifications.
Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015
Verification and Control of Partially Observable Probabilistic Real-Time Systems.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2015
The Hanoi Omega-Automata Format.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015
Nested Value Iteration for Partially Satisfiable Co-Safe LTL Specifications (Extended Abstract).
Proceedings of the 2015 AAAI Fall Symposia, Arlington, Virginia, USA, November 12-14, 2015, 2015
2014
Local abstraction refinement for probabilistic timed programs.
Theor. Comput. Sci., 2014
Optimal and dynamic planning for Markov decision processes with co-safe LTL specifications.
Proceedings of the 2014 IEEE/RSJ International Conference on Intelligent Robots and Systems, 2014
On Incremental Quantitative Verification for Probabilistic Systems.
Proceedings of the HOWARD-60: A Festschrift on the Occasion of Howard Barringer's 60th Birthday, 2014
Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations.
Proceedings of the Horizons of the Mind. A Tribute to Prakash Panangaden, 2014
Verification of Markov Decision Processes Using Learning Algorithms.
Proceedings of the Automated Technology for Verification and Analysis, 2014
2013
Compositional probabilistic verification through multi-objective model checking.
Inf. Comput., 2013
Model checking for probabilistic timed automata.
Formal Methods Syst. Des., 2013
Automatic verification of competitive stochastic systems.
Formal Methods Syst. Des., 2013
Strategic Analysis of Trust Models for User-Centric Networks
Proceedings of the Proceedings 1st International Workshop on Strategic Reasoning, 2013
SMT-Based Bisimulation Minimisation of Markov Models.
Proceedings of the Verification, 2013
PRISM-games: A Model Checker for Stochastic Multi-Player Games.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013
Probabilistic Point-to-Point Information Leakage.
Proceedings of the 2013 IEEE 26th Computer Security Foundations Symposium, 2013
Automated Verification and Strategy Synthesis for Probabilistic Systems.
Proceedings of the Automated Technology for Verification and Analysis, 2013
2012
Advances in Probabilistic Model Checking.
Proceedings of the Software Safety and Security - Tools for Analysis and Verification, 2012
Evaluation of Sustained Stochastic Oscillations by Means of a System of Differential Equations.
Int. J. Comput. Their Appl., 2012
Probabilistic verification of Herman's self-stabilisation algorithm.
Formal Aspects Comput., 2012
Incremental Runtime Verification of Probabilistic Systems.
Proceedings of the Runtime Verification, Third International Conference, 2012
The PRISM Benchmark Suite.
Proceedings of the Ninth International Conference on Quantitative Evaluation of Systems, 2012
Pareto Curves for Probabilistic Model Checking.
Proceedings of the Automated Technology for Verification and Analysis, 2012
2011
Quantitative Multi-objective Verification for Probabilistic Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011
Automated Verification Techniques for Probabilistic Systems.
Proceedings of the Formal Methods for Eternal Networked Software Systems, 2011
Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems.
Proceedings of the Eighth International Conference on Quantitative Evaluation of Systems, 2011
Automated Learning of Probabilistic Assumptions for Compositional Reasoning.
Proceedings of the Fundamental Approaches to Software Engineering, 2011
Incremental quantitative verification for Markov decision processes.
Proceedings of the 2011 IEEE/IFIP International Conference on Dependable Systems and Networks, 2011
Verifying Team Formation Protocols with Probabilistic Model Checking.
Proceedings of the Computational Logic in Multi-Agent Systems, 2011
PRISM 4.0: Verification of Probabilistic Real-Time Systems.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011
A Systematic Approach to Evaluate Sustained Stochastic Oscillations.
Proceedings of the ISCA 3rd International Conference on Bioinformatics and Computational Biology, 2011
Learning-Based Compositional Verification for Synchronous Probabilistic Systems.
Proceedings of the Automated Technology for Verification and Analysis, 2011
2010
A game-based abstraction-refinement framework for Markov decision processes.
Formal Methods Syst. Des., 2010
Assume-Guarantee Verification for Probabilistic Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010
Compositional Verification of Probabilistic Systems Using Learning.
Proceedings of the QEST 2010, 2010
A Framework for Verification of Software with Time and Probabilities.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2010
Advances and challenges of probabilistic model checking.
Proceedings of the 48th Annual Allerton Conference on Communication, 2010
2009
Model Checking Probabilistic and Stochastic Extensions of the pi-Calculus.
IEEE Trans. Software Eng., 2009
Probabilistic Mobile Ambients.
Theor. Comput. Sci., 2009
PRISM: probabilistic model checking for performance and reliability analysis.
SIGMETRICS Perform. Evaluation Rev., 2009
Abstraction Refinement for Probabilistic Software.
Proceedings of the Verification, 2009
Language-Level Symmetry Reduction for Probabilistic Model Checking.
Proceedings of the QEST 2009, 2009
Bisimulation for Demonic Schedulers.
Proceedings of the Foundations of Software Science and Computational Structures, 2009
Stochastic Games for Verification of Probabilistic Timed Automata.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2009
Quantitative Verification Techniques for Biological Processes.
Proceedings of the Algorithmic Bioprocesses, 2009
2008
Probabilistic model checking of complex biological pathways.
Theor. Comput. Sci., 2008
Analysis of a gossip protocol in PRISM.
SIGMETRICS Perform. Evaluation Rev., 2008
Using probabilistic model checking in systems biology.
SIGMETRICS Perform. Evaluation Rev., 2008
Game-Based Probabilistic Predicate Abstraction in PRISM.
Proceedings of the Sixth Workshop on Quantitative Aspects of Programming Languages, 2008
Generating Compact MTBDD-Representations from ProbmelaSpecifications.
Proceedings of the Model Checking Software, 2008
Symbolic Magnifying Lens Abstraction in Markov Decision Processes.
Proceedings of the Fifth International Conference on the Quantitative Evaluaiton of Systems (QEST 2008), 2008
2007
Stochastic Model Checking.
Proceedings of the Formal Methods for Performance Evaluation, 2007
Model checking the probabilistic pi-calculus.
Proceedings of the Fourth International Conference on the Quantitative Evaluaiton of Systems (QEST 2007), 2007
GRIP: Generic Representatives in PRISM.
Proceedings of the Fourth International Conference on the Quantitative Evaluaiton of Systems (QEST 2007), 2007
2006
Numerical vs. statistical probabilistic model checking.
Int. J. Softw. Tools Technol. Transf., 2006
A formal analysis of bluetooth device discovery.
Int. J. Softw. Tools Technol. Transf., 2006
Performance analysis of probabilistic timed automata using digital clocks.
Formal Methods Syst. Des., 2006
Simulation and verification for computational modelling of signalling pathways.
Proceedings of the Winter Simulation Conference WSC 2006, 2006
PRISM: A Tool for Automatic Verification of Probabilistic Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006
Game-based Abstraction for Markov Decision Processes.
Proceedings of the Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), 2006
On Reduction Criteria for Probabilistic Reward Models.
Proceedings of the FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 2006
Symmetry Reduction for Probabilistic Model Checking.
Proceedings of the Computer Aided Verification, 18th International Conference, 2006
2005
Evaluating the reliability of NAND multiplexing with PRISM.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2005
Probabilistic model checking in practice: case studies with PRISM.
SIGMETRICS Perform. Evaluation Rev., 2005
Using probabilistic model checking for dynamic power management.
Formal Aspects Comput., 2005
Quantitative Analysis With the Probabilistic Model Checker PRISM.
Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages, 2005
A Wavefront Parallelisation of CTMC Solution Using MTBDDs.
Proceedings of the 2005 International Conference on Dependable Systems and Networks (DSN 2005), 28 June, 2005
2004
Probabilistic symbolic model checking with PRISM: a hybrid approach.
Int. J. Softw. Tools Technol. Transf., 2004
Symbolic Representations and Analysis of Large Probabilistic Systems.
Proceedings of the Validation of Stochastic Systems - A Guide to Current Research, 2004
Evaluating the Reliability of Defect-Tolerant Architectures for Nanotechnology with Probabilistic Model Checking.
Proceedings of the 17th International Conference on VLSI Design (VLSI Design 2004), 2004
Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004
PRISM 2.0: A Tool for Probabilistic Model Checking.
Proceedings of the 1st International Conference on Quantitative Evaluation of Systems (QEST 2004), 2004
Dual-Processor Parallelisation of Symbolic Probabilistic Model Checking.
Proceedings of the 12th International Workshop on Modeling, 2004
Mathematical techniques for analyzing concurrent and probabilistic systems.
CRM monograph series 23, American Mathematical Society, ISBN: 978-0-8218-3571-5, 2004
2003
Implementation of symbolic model checking for probabilistic systems.
PhD thesis, 2003
On the use of MTBDDs for performability analysis and verification of stochastic systems.
J. Log. Algebraic Methods Program., 2003
2002
A Symbolic Out-of-Core Solution Method for Markov Models.
Proceedings of the Parallel and Distributed Model Checking, 2002
Formal analysis and validation of continuous-time Markov chain based system level power management strategies.
Proceedings of the Seventh IEEE International High-Level Design Validation and Test Workshop 2002, 2002
Computer Based Real-Time Simulator for Renewable Energy Converters.
Proceedings of the 1st IEEE International Workshop on Electronic Design, 2002
PRISM: Probabilistic Symbolic Model Checker.
Proceedings of the Computer Performance Evaluation, 2002
2001
Faster and Symbolic CTMC Model Checking.
Proceedings of the Process Algebra and Probabilistic Methods, 2001
2000
Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 2000