Project Publications
Sort by: date, type, title
31 publications:
-
[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]
-
[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]
-
[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]
-
[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]
-
[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]
-
[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]
-
[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]
-
[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]
-
[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]
-
[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]
-
[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]
-
[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]
-
[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]
-
[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]
-
[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]
-
[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]
Sort by: date, type, title
