PRISM Publications
The following is a list of all PRISM-related papers authored or co-authored by members of the PRISM team.
We also have lists of
all PRISM-related papers
and
external PRISM-related papers.
Sort by: date, type, title
101 publications:
-
[KNP09c]
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), Springer. To appear.
September 2009.
[pdf]
[bib]
-
[JKNT09]
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), Springer. To appear.
September 2009.
[pdf]
[bib]
-
[DMP09]
A. Donaldson, A. Miller and D. Parker.
Language-level Symmetry Reduction for Probabilistic Model Checking.
In Proc. 6th International Conference on Quantitative Evaluation of Systems (QEST'09). To appear.
September 2009.
[pdf]
[bib]
-
[KNP09b]
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, Springer. To appear.
July 2009.
[ps.gz]
[pdf]
[bib]
-
[Kwi09]
M. Kwiatkowska.
On Quantitative Software Verification.
In C. Pasareanu (editor) Proc. 16th International SPIN Workshop, volume 5578 of LNCS, pages 2-3, Springer. Invited contribution.
June 2009.
[bib]
-
[CK09]
R. Calinescu and M. Kwiatkowska.
Using Quantitative Analysis to Implement Autonomic IT Systems.
In Proc. 31st International Conference on Software Engineering (ICSE 2009). To appear.
May 2009.
[pdf]
[bib]
-
[KH09]
M. Kattenbelt and M. Huth.
Abstraction Framework for Markov Decision Processes and PCTL Via Games.
Technical report RR-09-01, Oxford University Computing Laboratory.
March 2009.
[pdf]
-
[KNP09a]
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.
March 2009.
[pdf]
[bib]
-
[NPPW09]
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.
March 2009.
[pdf]
[bib]
-
[KNPV09]
M. Kwiatkowska, G. Norman, D. Parker and M.G. Vigliotti.
Probabilistic Mobile Ambients.
Theoretical Computer Science, 410(12-13), pages 1272-1303.
March 2009.
[ps.gz]
[pdf]
[bib]
-
[CK09b]
R. Calinescu and M. Kwiatkowska.
CADS*: Computer-Aided Development of Self-* Systems.
In Marsha Chechik and Martin Wirsing (editors) Fundamental Approaches to Software Engineering (FASE 2009), volume 5503 of Lecture Notes in Computer Science, pages 421-424, Springer-Verlag.
March 2009.
[pdf]
[bib]
-
[KKNP09]
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.
[ps.gz]
[pdf]
[bib]
-
[KNP09e]
M. Kwiatkowska, G. Norman and D. Parker.
Probabilistic Model Checking for Systems Biology.
In Symbolic Systems Biology, Jones and Bartlett. To appear.
2009.
[bib]
-
[EKVY08]
K. Etessami, M. Kwiatkowska, M. Vardi and M. Yannakakis.
Multi-Objective Model Checking of Markov Decision Processes.
Logical Methods in Computer Science, 4(4), pages 1-21.
2008.
[pdf]
[bib]
-
[Ma08]
Zhongdan Ma.
Modelling with PRISM of Intelligent System.
Masters thesis, University of Oxford.
2008.
[pdf]
[bib]
-
[KNP08d]
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]
-
[RPNdA08]
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]
-
[CK08]
R. Calinescu and M. Kwiatkowska.
Software Engineering Techniques for the Development of Systems of Systems.
In Proc. 15th Monterey Workshop on Foundations of Computer Software, pages 86--93.
September 2008.
[pdf]
[bib]
-
[CBGP08]
F. Ciesinski, C. Baier, M. Groesser and D. Parker.
Generating compact MTBDD-representations from Probmela specifications.
In Proc. 15th International SPIN Workshop on Model Checking of Software (SPIN'08), volume 5156 of Lecture Notes in Computer Science, pages 60-76, Springer.
August 2008.
[pdf]
[bib]
-
[KNP08a]
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.
[ps.gz]
[pdf]
[bib]
-
[KKNP08a]
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.
[ps.gz]
[pdf]
[bib]
-
[KKNP08c]
M. Kattenbelt, M. Kwiatkowska, G. Norman and D. Parker.
A Game-based Abstraction-Refinement Framework for Markov Decision Processes.
Technical report RR-08-06, Oxford University Computing Laboratory.
February 2008.
[ps.gz]
[pdf]
[bib]
-
[Sch08]
O. Schaeffer.
On the use of process algebra techniques in computational modelling of cancer initiation and development.
Ph.D. thesis, University of Birmingham.
February 2008.
[pdf]
[bib]
-
[HKN+08]
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.
February 2008.
[ps.gz]
[pdf]
[bib]
-
[KNPS08]
M. Kwiatkowska, G. Norman, D. Parker and J. Sproston.
Verification of Real-Time Probabilistic Systems.
In Modeling and Verification of Real-Time Systems: Formalisms and Software Tools, pages 249-288, John Wiley & Sons.
January 2008.
[bib]
-
[DKN+07]
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 Handbook of Formal Methods in Industrial Critical Systems (FMICS). To appear.
2007.
[pdf]
[bib]
-
[KNP07b]
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.
[ps.gz]
[pdf]
[bib]
-
[NPPW07]
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.
[ps.gz]
[pdf]
[bib]
-
[DMP07]
A. Donaldson, A. Miller and D. Parker.
GRIP: Generic Representatives in PRISM.
In Proc. 4th International Conference on Quantitative Evaluation of Systems (QEST'07), pages 115-116, IEEE CS Press.
September 2007.
[ps.gz]
[pdf]
[bib]
-
[Kwi07]
M. Kwiatkowska.
Quantitative Verification: Models, Techniques and Tools.
In Proc. 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), pages 449-458, ACM Press.
September 2007.
[pdf]
[bib]
-
[FMM07]
A. Fehnker, M. Fruth and A. McIver.
Graphical modelling for simulation and formal analysis of wireless network protocols.
In Proc. Workshop on Methods, Models and Tools for Fault-Tolerance (MeMoT'07) at the 7th International Conference on Integrated Formal Methods (IFM'07), pages 80-87. Technical Report CS-TR-1032, University of Newcastle upon Tyne.
July 2007.
[pdf]
[bib]
-
[KNSW07]
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.
[ps.gz]
[pdf]
[bib]
-
[KNP07a]
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, volume 4486 of Lecture Notes in Computer Science (Tutorial Volume), pages 220-270, Springer.
June 2007.
[ps.gz]
[pdf]
[bib]
-
[EKVY07]
K. Etessami, M. Kwiatkowska, M. Vardi and M. Yannakakis.
Multi-Objective Model Checking of Markov Decision Processes.
In Proc. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), volume 4424 of LNCS, pages 50-65, Springer.
March 2007.
[pdf]
[bib]
-
[GNB+06]
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.
[ps.gz]
[pdf]
[bib]
-
[SUH+06]
H. Sauro, A. Uhrmacher, D. Harel, M. Hucka, M. Kwiatkowska, P. Mendes, C. Shaffer, L. Stromback and J. Tyson.
Challenges for modeling and simulation methods in systems biology.
In L. Perrone, F. Wieland, J. Liu, B. Lawson, D. Nicol and R. Fujimoto (editors) Proc. 2006 Winter Simulation Conference, pages 1720-1730, IEEE.
December 2006.
[pdf]
[bib]
-
[KNP+06]
M. Kwiatkowska, G. Norman, D. Parker, O. Tymchyshyn, J. Heath and E. Gaffney.
Simulation and verification for computational modelling of signalling pathways.
In L. F. Perrone, F. P. Wieland, J. Liu, B. G. Lawson, D. M. Nicol, and R. M. Fujimoto (editors) Proceedings of the 2006 Winter Simulation Conference, pages 1666-1674, Winter Simulation Conference.
December 2006.
[ps.gz]
[pdf]
[bib]
-
[DKNP06]
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.
[ps.gz]
[pdf]
[bib]
-
[Fru06]
M. Fruth.
Probabilistic Model Checking of Contention Resolution in the IEEE 802.15.4 Low-Rate Wireless Personal Area Network Protocol.
In Proc. 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'06).
November 2006.
[pdf]
[bib]
-
[NS06]
G. Norman and V. Shmatikov.
Analysis of Probabilistic Contract Signing.
Journal of Computer Security, 14(6), pages 561-589, IOS Press.
November 2006.
[ps.gz]
[pdf]
[bib]
-
[HKN+06]
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.
[ps.gz]
[pdf]
[bib]
-
[Wan06]
F. Wang.
Symbolic Implementation of Model-Checking Probabilistic Timed Automata.
Ph.D. thesis, University of Birmingham.
September 2006.
[pdf]
[bib]
-
[KNP06b]
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.
[ps.gz]
[pdf]
[bib]
-
[KNPS06]
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.
[ps.gz]
[pdf]
[bib]
-
[KNP06a]
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.
[ps.gz]
[pdf]
[bib]
-
[YKNP06]
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), Springer. 216-228.
June 2006.
[ps.gz]
[pdf]
[bib]
-
[HKNP06]
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.
[ps.gz]
[pdf]
[bib]
-
[KNP06e]
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.
[ps.gz]
[pdf]
[bib]
-
[WK05]
F. Wang and M. Kwiatkowska.
An MTBDD-based implementation of forward reachability for probabilistic timed automata.
In Proc. 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA'05), volume 3707 of Lecture Notes in Computer Science, pages 385-399, Springer.
October 2005.
[ps.gz]
[pdf]
[bib]
-
[NPKS05]
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.
[ps.gz]
[pdf]
[bib]
-
[ZPK05b]
Y. Zhang, D. Parker and M. Kwiatkowska.
Grid-enabled Probabilistic Model Checking with PRISM.
In Proc. 4th All Hands Meeting Workshop (AHM'05).
September 2005.
[ps.gz]
[pdf]
[bib]
-
[KNP05c]
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.
[ps.gz]
[pdf]
[bib]
-
[NPK+05]
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.
[ps.gz]
[pdf]
[bib]
-
[ZPK05a]
Y. Zhang, D. Parker and M. Kwiatkowska.
A Wavefront Parallelisation of CTMC Solution using MTBDDs.
In Proc. International Conference on Dependable Systems and Networks (DSN'05), pages 732-742, IEEE CS Press.
June 2005.
[ps.gz]
[pdf]
[bib]
-
[KNP05d]
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.
[ps.gz]
[pdf]
[bib]
-
[Hin05]
A. Hinton.
Software Project M60: Simulator for the Probabilistic Model Checker PRISM.
MEng Final Year Project Dissertation, School of Computer Science, University of Birmingham.
April 2005.
[ps.gz]
[pdf]
[bib]
-
[KNP05b]
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.
[ps.gz]
[pdf]
[bib]
-
[DKNP04]
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.
[ps.gz]
[pdf]
[bib]
-
[Meh04b]
R. Mehmood.
Disk-based techniques for efficient solution of large Markov chains.
Ph.D. thesis, University of Birmingham.
October 2004.
[ps.gz]
[pdf]
[bib]
-
[Nor04]
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.
[ps.gz]
[pdf]
[bib]
-
[KPZM04]
M. Kwiatkowska, D. Parker, Y. Zhang and R. Mehmood.
Dual-Processor Parallelisation of Symbolic Probabilistic Model Checking.
In Proc. 12th International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS'04), pages 123-130, IEEE CS Press.
October 2004.
[ps.gz]
[pdf]
[bib]
-
[DFH+04]
M. Duflot, L. Fribourg, T. Hérault, R. Lassaigne, F. Magniette, S. Messika, S. Peyronnet and C. Picaronny.
Probabilistic model checking of the CSMA/CD protocol using PRISM and APMC.
In Proc. 4th Workshop on Automated Verification of Critical Systems (AVoCS'04), volume 128(6) of Electronic Notes in Theoretical Computer Science, pages 195-214, Elsevier Science.
September 2004.
[ps.gz]
[pdf]
[bib]
-
[KNP04b]
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.
[ps.gz]
[pdf]
[bib]
-
[KNSW04]
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.
[ps.gz]
[pdf]
[bib]
-
[KNP04d]
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.
[ps.gz]
[pdf]
[bib]
-
[MP04]
A. Miner and D. Parker.
Symbolic Representations and Analysis of Large Probabilistic Systems.
In Validation of Stochastic Systems: A Guide to Current Research, volume 2925 of Lecture Notes in Computer Science.
August 2004.
[ps.gz]
[pdf]
[bib]
-
[Meh04a]
R. Mehmood.
Serial Disk-based Analysis of Large Stochastic Models.
In Validation of Stochastic Systems: A Guide to Current Research, volume 2925 of Lecture Notes in Computer Science, Springer-Verlag.
August 2004.
[ps.gz]
[pdf]
[bib]
-
[KNP04c]
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), Elsevier.
April 2004.
[ps.gz]
[pdf]
[bib]
-
[YKNP04]
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.
[ps.gz]
[pdf]
[bib]
-
[DKN04]
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.
[ps.gz]
[pdf]
[bib]
-
[KNP04a]
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]
-
[NPKS04]
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.
[ps.gz]
[pdf]
[bib]
-
[MPK03b]
R. Mehmood, D. Parker and M. Kwiatkowska.
An Efficient BDD-Based Implementation of Gauss-Seidel for CTMC Analysis.
Technical report CSR-03-13, School of Computer Science, University of Birmingham.
December 2003.
[ps.gz]
[pdf]
[bib]
-
[KNS03d]
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.
[ps.gz]
[pdf]
[bib]
-
[KNPS03]
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).
September 2003.
[ps.gz]
[pdf]
[bib]
-
[MPK03a]
R. Mehmood, D. Parker and M. Kwiatkowska.
An Efficient Symbolic Out-of-Core Solution Method for Markov Models.
Technical report CSR-03-08, School of Computer Science, University of Birmingham.
August 2003.
[ps.gz]
[pdf]
[bib]
-
[Kwi03]
M. Kwiatkowska.
Model Checking for Probability and Time: From Theory to Practice.
In Proc. 18th IEEE Symposium on Logic in Computer Science (LICS'03), pages 351-360, IEEE CS Press. Invited paper.
June 2003.
[ps.gz]
[pdf]
[bib]
-
[HKN+03]
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.
[ps.gz]
[pdf]
[bib]
-
[NPK+03]
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.
[ps.gz]
[pdf]
[bib]
-
[KNS03b]
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.
[ps.gz]
[pdf]
[bib]
-
[NS02]
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.
[ps.gz]
[pdf]
[bib]
-
[KN02]
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.
[ps.gz]
[pdf]
[bib]
-
[NPK+02]
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.
[ps.gz]
[pdf]
[bib]
-
[KNP02d]
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.
[ps.gz]
[pdf]
[bib]
-
[Par02]
D. Parker.
Implementation of Symbolic Model Checking for Probabilistic Systems.
Ph.D. thesis, University of Birmingham.
August 2002.
[ps.gz]
[pdf]
[bib]
-
[KMNP02]
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.
[ps.gz]
[pdf]
[bib]
-
[KM02]
M. Kwiatkowska and R. Mehmood.
Out-of-Core Solution of Large Linear Systems of Equations arising from Stochastic Modelling.
In Proc. PAPM/PROBMIV'02, volume 2399 of LNCS, pages 135-151, Springer-Verlag.
July 2002.
[ps.gz]
[bib]
-
[DKN02]
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.
[ps.gz]
[pdf]
[bib]
-
[KNS02a]
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.
[ps.gz]
[pdf]
[bib]
-
[KNP02c]
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.
[ps.gz]
[pdf]
[bib]
-
[KNSS02]
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.
[ps.gz]
[pdf]
[bib]
-
[KNP02b]
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.
[ps.gz]
[pdf]
[bib]
-
[KNP02a]
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.
[ps.gz]
[pdf]
[bib]
-
[Spr01]
J. Sproston.
Model Checking for Probabilistic Timed and Hybrid Systems.
Ph.D. thesis, School of Computer Science, The University of Birmingham.
2001.
[ps.gz]
[bib]
-
[KKNP01]
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.
[ps.gz]
[pdf]
[bib]
-
[KNP01]
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.
[ps.gz]
[pdf]
[bib]
-
[KNS01b]
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 LNCS, pages 169--183, Springer.
August 2001.
[ps.gz]
[pdf]
[bib]
-
[KNS01a]
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.
[ps.gz]
[pdf]
[bib]
Sort by: date, type, title
