Project Publications
Sort by: date, type, title
31 publications:
-
[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]
-
[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]
-
[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]
-
[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]
-
[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]
-
[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]
-
[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]
-
[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]
-
[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), volume 2791 of LNCS, pages 105-120, Springer.
September 2003.
[ps.gz]
[pdf]
[bib]
-
[CK03]
S. Cattani and M. Kwiatkowska.
CSP + Clocks: a process algebra for timed automata.
In M. Leuschel and S. Gruner and S. Lo Presti (editors), Proc. 3rd Workshop on Automated Verification of Critical Systems (AVoCS'03), pages 50-63.
April 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]
-
[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]
-
[CS02]
S. Cattani and R. Segala.
Decision algorithms for probabilistic bisimulation.
In L. Brim and P. Janar and M. Ketinsky and A. Kuera (editors), Proc. 14th International Conference on Concurrency Theory (CONCUR'02), volume 2421 of Lecture Notes in Computer Science, pages 371-385, Springer.
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]
-
[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]
-
[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]
-
[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]
-
[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]
-
[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]
-
[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]
-
[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]
-
[KNSS00a]
M. Kwiatkowska, G. Norman, R. Segala and J. Sproston.
Verifying Quantitative Properties of Continuous Probabilistic Timed Automata.
In C. Palamidessi (editor), Proc. CONCUR 2000 - Concurrency Theory, volume 1877 of Lecture Notes in Computer Science, pages 123-137, Springer.
August 2000.
[ps.gz]
[pdf]
[bib]
-
[Spr00]
J. Sproston.
Decidable Model Checking of Probabilistic Hybrid Automata.
In Proc. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'00), volume 1926 of LNCS, pages 31-45, Springer.
2000.
[ps.gz]
[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]
-
[KNS03c]
M. Kwiatkowska, G. Norman and J. Sproston.
PCTL model checking of symbolic probabilistic systems.
Technical report CSR-03-2, University of Birmingham, School of Computer Science.
April 2003.
[ps.gz]
[pdf]
[bib]
-
[KNS03a]
M. Kwiatkowska, G. Norman and J. Sproston.
Symbolic Computation of Minimal Probabilistic Reachability.
Technical report CSR-03-01, University of Birmingham, School of Computer Science.
January 2003.
[ps.gz]
[pdf]
[bib]
-
[KNS00]
M. Kwiatkowska, G. Norman and J. Sproston.
Symbolic Model Checking of Probabilistic Timed Automata Using Backwards Reachability.
Technical report CSR-00-01, University of Birmingham, School of Computer Science.
January 2000.
[ps.gz]
[pdf]
[bib]
Sort by: date, type, title
