@article{KwiatkowskaNSS02,
  title = {Automatic verification of real-time systems with discrete probability distributions},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and Roberto Segala and Jeremy Sproston},
  year = {2002},
  doi = {10.1016/S0304-3975(01)00046-9},
  url = {http://dx.doi.org/10.1016/S0304-3975(01)00046-9},
  researchr = {https://researchr.org/publication/KwiatkowskaNSS02},
  cites = {0},
  citedby = {0},
  journal = {TCS},
  volume = {282},
  number = {1},
  pages = {101-150},
}

@article{KwiatkowskaNP08,
  title = {Using probabilistic model checking in systems biology},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and David Parker},
  year = {2008},
  doi = {10.1145/1364644.1364651},
  url = {http://doi.acm.org/10.1145/1364644.1364651},
  tags = {model checking, meta-model, Meta-Environment},
  researchr = {https://researchr.org/publication/KwiatkowskaNP08},
  cites = {0},
  citedby = {0},
  journal = {sigmetrics},
  volume = {35},
  number = {4},
  pages = {14-21},
}

@article{KwiatkowskaNPV09,
  title = {Probabilistic Mobile Ambients},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and David Parker and Maria Grazia Vigliotti},
  year = {2009},
  doi = {10.1016/j.tcs.2008.12.058},
  url = {http://dx.doi.org/10.1016/j.tcs.2008.12.058},
  tags = {mobile},
  researchr = {https://researchr.org/publication/KwiatkowskaNPV09},
  cites = {0},
  citedby = {0},
  journal = {TCS},
  volume = {410},
  number = {12-13},
  pages = {1272-1303},
}

@article{KwiatkowskaNP06:0,
  title = {Quantitative Analysis With the Probabilistic Model Checker PRISM},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and David Parker},
  year = {2006},
  doi = {10.1016/j.entcs.2005.10.030},
  url = {http://dx.doi.org/10.1016/j.entcs.2005.10.030},
  tags = {analysis},
  researchr = {https://researchr.org/publication/KwiatkowskaNP06%3A0},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {153},
  number = {2},
  pages = {5-31},
}

@article{NormanS06:0,
  title = {Analysis of probabilistic contract signing},
  author = {Gethin J. Norman and Vitaly Shmatikov},
  year = {2006},
  url = {http://iospress.metapress.com/openurl.asp?genre=article&issn=0926-227X&volume=14&issue=6&spage=561},
  tags = {contracts, analysis},
  researchr = {https://researchr.org/publication/NormanS06%3A0},
  cites = {0},
  citedby = {0},
  journal = {jcs},
  volume = {14},
  number = {6},
  pages = {561-589},
}

@article{KwiatkowskaNP04:0,
  title = {Probabilistic symbolic model checking with PRISM: a hybrid approach},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and David Parker},
  year = {2004},
  url = {http://www.springerlink.com/index/10.1007/s10009-004-0140-2},
  tags = {model checking, meta-model, Meta-Environment, systematic-approach},
  researchr = {https://researchr.org/publication/KwiatkowskaNP04%3A0},
  cites = {0},
  citedby = {0},
  journal = {STTT},
  volume = {6},
  number = {2},
  pages = {128-142},
}

@inproceedings{HintonKNP06,
  title = {PRISM: A Tool for Automatic Verification of Probabilistic Systems},
  author = {Andrew Hinton and Marta Z. Kwiatkowska and Gethin J. Norman and David Parker},
  year = {2006},
  doi = {10.1007/11691372_29},
  url = {http://dx.doi.org/10.1007/11691372_29},
  researchr = {https://researchr.org/publication/HintonKNP06},
  cites = {0},
  citedby = {0},
  pages = {441-444},
  booktitle = {TACAS},
}

@inproceedings{KwiatkowskaNPQ10,
  title = {Assume-Guarantee Verification for Probabilistic Systems},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and David Parker and Hongyang Qu},
  year = {2010},
  doi = {10.1007/978-3-642-12002-2_3},
  url = {http://dx.doi.org/10.1007/978-3-642-12002-2_3},
  researchr = {https://researchr.org/publication/KwiatkowskaNPQ10},
  cites = {0},
  citedby = {0},
  pages = {23-37},
  booktitle = {TACAS},
}

@article{HeathKNPT08,
  title = {Probabilistic model checking of complex biological pathways},
  author = {John Heath and Marta Z. Kwiatkowska and Gethin J. Norman and David Parker and Oksana Tymchyshyn},
  year = {2008},
  doi = {10.1016/j.tcs.2007.11.013},
  url = {http://dx.doi.org/10.1016/j.tcs.2007.11.013},
  tags = {model checking, meta-model, Meta-Environment},
  researchr = {https://researchr.org/publication/HeathKNPT08},
  cites = {0},
  citedby = {0},
  journal = {TCS},
  volume = {391},
  number = {3},
  pages = {239-257},
}

@article{KwiatkowskaMNP02,
  title = {A Symbolic Out-of-Core Solution Method for Markov Models},
  author = {Marta Z. Kwiatkowska and Rashid Mehmood and Gethin J. Norman and David Parker},
  year = {2002},
  url = {http://www.elsevier.com/gej-ng/31/29/23/121/49/show/Products/notes/index.htt#011},
  tags = {Markov},
  researchr = {https://researchr.org/publication/KwiatkowskaMNP02},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {68},
  number = {4},
  pages = {589-604},
}

@inproceedings{HeathKNPT06,
  title = {Probabilistic Model Checking of Complex Biological Pathways},
  author = {John Heath and Marta Z. Kwiatkowska and Gethin J. Norman and David Parker and Oksana Tymchyshyn},
  year = {2006},
  doi = {10.1007/11885191_3},
  url = {http://dx.doi.org/10.1007/11885191_3},
  tags = {model checking, meta-model, Meta-Environment},
  researchr = {https://researchr.org/publication/HeathKNPT06},
  cites = {0},
  citedby = {0},
  pages = {32-47},
  booktitle = {cmsb},
}

@article{NormanPKS05,
  title = {Evaluating the reliability of NAND multiplexing with PRISM},
  author = {Gethin J. Norman and David Parker and Marta Z. Kwiatkowska and Sandeep K. Shukla},
  year = {2005},
  doi = {10.1109/TCAD.2005.852033},
  url = {http://dx.doi.org/10.1109/TCAD.2005.852033},
  tags = {reliability},
  researchr = {https://researchr.org/publication/NormanPKS05},
  cites = {0},
  citedby = {0},
  journal = {tcad},
  volume = {24},
  number = {10},
  pages = {1629-1637},
}

@inproceedings{KwiatkowskaNPTHG06,
  title = {Simulation and verification for computational modelling of signalling pathways},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and David Parker and Oksana Tymchyshyn and John Heath and Eamonn Gaffney},
  year = {2006},
  doi = {10.1145/1218112.1218415},
  url = {http://doi.acm.org/10.1145/1218112.1218415},
  researchr = {https://researchr.org/publication/KwiatkowskaNPTHG06},
  cites = {0},
  citedby = {0},
  pages = {1666-1674},
  booktitle = {wsc},
}

@inproceedings{KwiatkowskaNSS99,
  title = {Automatic Verification of Real-Time Systems with Discrete Probability Distributions},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and Roberto Segala and Jeremy Sproston},
  year = {1999},
  url = {http://link.springer.de/link/service/series/0558/bibs/1601/16010075.htm},
  researchr = {https://researchr.org/publication/KwiatkowskaNSS99},
  cites = {0},
  citedby = {0},
  pages = {75-95},
  booktitle = {arts},
}

@inproceedings{KwiatkowskaNP06,
  title = {Game-based Abstraction for Markov Decision Processes},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and David Parker},
  year = {2006},
  doi = {10.1109/QEST.2006.19},
  url = {http://doi.ieeecomputersociety.org/10.1109/QEST.2006.19},
  tags = {rule-based, Markov, abstraction},
  researchr = {https://researchr.org/publication/KwiatkowskaNP06},
  cites = {0},
  citedby = {0},
  pages = {157-166},
  booktitle = {qest},
}

@article{DuflotKNP06,
  title = {A formal analysis of bluetooth device discovery},
  author = {Marie Duflot and Marta Z. Kwiatkowska and Gethin J. Norman and David Parker},
  year = {2006},
  doi = {10.1007/s10009-006-0014-x},
  url = {http://dx.doi.org/10.1007/s10009-006-0014-x},
  tags = {discovery, analysis},
  researchr = {https://researchr.org/publication/DuflotKNP06},
  cites = {0},
  citedby = {0},
  journal = {STTT},
  volume = {8},
  number = {6},
  pages = {621-632},
}

@inproceedings{KwiatkowskaNS01:0,
  title = {Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and Roberto Segala},
  year = {2001},
  url = {http://link.springer.de/link/service/series/0558/bibs/2102/21020194.htm},
  tags = {protocol},
  researchr = {https://researchr.org/publication/KwiatkowskaNS01%3A0},
  cites = {0},
  citedby = {0},
  pages = {194-206},
  booktitle = {cav},
}

@inproceedings{KatoenKNP01,
  title = {Faster and Symbolic CTMC Model Checking},
  author = {Joost-Pieter Katoen and Marta Z. Kwiatkowska and Gethin J. Norman and David Parker},
  year = {2001},
  url = {http://link.springer.de/link/service/series/0558/bibs/2165/21650023.htm},
  tags = {model checking, meta-model, Meta-Environment},
  researchr = {https://researchr.org/publication/KatoenKNP01},
  cites = {0},
  citedby = {0},
  pages = {23-38},
  booktitle = {papm},
}

@inproceedings{KwiatkowskaNS01,
  title = {Symbolic Computation of Maximal Probabilistic Reachability},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and Jeremy Sproston},
  year = {2001},
  url = {http://link.springer.de/link/service/series/0558/bibs/2154/21540169.htm},
  researchr = {https://researchr.org/publication/KwiatkowskaNS01},
  cites = {0},
  citedby = {0},
  pages = {169-183},
  booktitle = {concur},
}

@article{KwiatkowskaN98a,
  title = {A Testing Equivalence for Reactive Probabilistic Processes},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman},
  year = {1998},
  url = {http://www.elsevier.com/gej-ng/31/29/23/40/25/show/Products/notes/index.htt#006},
  tags = {testing},
  researchr = {https://researchr.org/publication/KwiatkowskaN98a},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {16},
  number = {2},
  pages = {114-132},
}

@article{NormanPKSG05,
  title = {Using probabilistic model checking for dynamic power management},
  author = {Gethin J. Norman and David Parker and Marta Z. Kwiatkowska and Sandeep K. Shukla and Rajesh Gupta},
  year = {2005},
  doi = {10.1007/s00165-005-0062-0},
  url = {http://dx.doi.org/10.1007/s00165-005-0062-0},
  tags = {model checking, meta-model, Meta-Environment},
  researchr = {https://researchr.org/publication/NormanPKSG05},
  cites = {0},
  citedby = {0},
  journal = {fac},
  volume = {17},
  number = {2},
  pages = {160-176},
}

@inproceedings{KwiatkowskaNP02,
  title = {Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and David Parker},
  year = {2002},
  url = {http://link.springer.de/link/service/series/0558/bibs/2280/22800052.htm},
  tags = {model checking, meta-model, Meta-Environment, systematic-approach},
  researchr = {https://researchr.org/publication/KwiatkowskaNP02},
  cites = {0},
  citedby = {0},
  pages = {52-66},
  booktitle = {TACAS},
}

@inproceedings{KwiatkowskaN02,
  title = {Verifying Randomized Byzantine Agreement},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman},
  year = {2002},
  url = {http://link.springer.de/link/service/series/0558/bibs/2529/25290194.htm},
  researchr = {https://researchr.org/publication/KwiatkowskaN02},
  cites = {0},
  citedby = {0},
  pages = {194-209},
  booktitle = {forte},
}

@inproceedings{KwiatkowskaNSW04,
  title = {Symbolic Model Checking for Probabilistic Timed Automata},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and Jeremy Sproston and Fuzhi Wang},
  year = {2004},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3253&spage=293},
  tags = {model checking, meta-model, Meta-Environment},
  researchr = {https://researchr.org/publication/KwiatkowskaNSW04},
  cites = {0},
  citedby = {0},
  pages = {293-308},
  booktitle = {formats},
}

@inproceedings{Norman04:0,
  title = {Analysing Randomized Distributed Algorithms},
  author = {Gethin J. Norman},
  year = {2004},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2925&spage=384},
  researchr = {https://researchr.org/publication/Norman04%3A0},
  cites = {0},
  citedby = {0},
  pages = {384-418},
  booktitle = {voss},
}

@article{KwiatkowskaN98,
  title = {A Fully Abstract Metric-Space Denotational Semantics for Reactive Probabilistic Processes},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman},
  year = {1998},
  url = {http://www.elsevier.com/gej-ng/31/29/23/37/23/show/Products/notes/index.htt#014},
  tags = {semantics, denotational semantics},
  researchr = {https://researchr.org/publication/KwiatkowskaN98},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {13},
  pages = {182},
}

@inproceedings{YounesKNP04,
  title = {Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study},
  author = {Håkan L. S. Younes and Marta Z. Kwiatkowska and Gethin J. Norman and David Parker},
  year = {2004},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2988&spage=46},
  tags = {empirical, model checking, meta-model, Meta-Environment},
  researchr = {https://researchr.org/publication/YounesKNP04},
  cites = {0},
  citedby = {0},
  pages = {46-60},
  booktitle = {TACAS},
}

@inproceedings{KwiatkowskaNSS00,
  title = {Verifying Quantitative Properties of Continuous Probabilistic Timed Automata},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and Roberto Segala and Jeremy Sproston},
  year = {2000},
  url = {http://link.springer.de/link/service/series/0558/bibs/1877/18770123.htm},
  researchr = {https://researchr.org/publication/KwiatkowskaNSS00},
  cites = {0},
  citedby = {0},
  pages = {123-137},
  booktitle = {concur},
}

@inproceedings{AlfaroKNPS00,
  title = {Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation},
  author = {Luca de Alfaro and Marta Z. Kwiatkowska and Gethin J. Norman and David Parker and Roberto Segala},
  year = {2000},
  url = {http://link.springer.de/link/service/series/0558/bibs/1785/17850395.htm},
  tags = {model checking, meta-model, Meta-Environment, process modeling},
  researchr = {https://researchr.org/publication/AlfaroKNPS00},
  cites = {0},
  citedby = {0},
  pages = {395-410},
  booktitle = {TACAS},
}

@article{DawsKN04,
  title = {Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM},
  author = {Conrado Daws and Marta Z. Kwiatkowska and Gethin J. Norman},
  year = {2004},
  url = {http://www.springerlink.com/index/10.1007/s10009-003-0118-5},
  tags = {protocol},
  researchr = {https://researchr.org/publication/DawsKN04},
  cites = {0},
  citedby = {0},
  journal = {STTT},
  volume = {5},
  number = {2-3},
  pages = {221-236},
}

@inproceedings{KattenbeltKNP09,
  title = {Abstraction Refinement for Probabilistic Software},
  author = {Mark Kattenbelt and Marta Z. Kwiatkowska and Gethin J. Norman and David Parker},
  year = {2009},
  doi = {10.1007/978-3-540-93900-9_17},
  url = {http://dx.doi.org/10.1007/978-3-540-93900-9_17},
  tags = {refinement, abstraction},
  researchr = {https://researchr.org/publication/KattenbeltKNP09},
  cites = {0},
  citedby = {0},
  pages = {182-197},
  booktitle = {vmcai},
}

@inproceedings{CattaniSKN05,
  title = {Stochastic Transition Systems for Continuous State Spaces and Non-determinism},
  author = {Stefano Cattani and Roberto Segala and Marta Z. Kwiatkowska and Gethin J. Norman},
  year = {2005},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3441&spage=125},
  researchr = {https://researchr.org/publication/CattaniSKN05},
  cites = {0},
  citedby = {0},
  pages = {125-139},
  booktitle = {fossacs},
}

@article{KwiatkowskaNSW07,
  title = {Symbolic model checking for probabilistic timed automata},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and Jeremy Sproston and Fuzhi Wang},
  year = {2007},
  doi = {10.1016/j.ic.2007.01.004},
  url = {http://dx.doi.org/10.1016/j.ic.2007.01.004},
  tags = {model checking, meta-model, Meta-Environment},
  researchr = {https://researchr.org/publication/KwiatkowskaNSW07},
  cites = {0},
  citedby = {0},
  journal = {iandc},
  volume = {205},
  number = {7},
  pages = {1027-1077},
}

@article{DawsKN02,
  title = {Automatic Verification of the IEEE-1394 Root Contention Protocol with KRONOS and PRISM},
  author = {Conrado Daws and Marta Z. Kwiatkowska and Gethin J. Norman},
  year = {2002},
  url = {http://www.elsevier.com/gej-ng/31/29/23/120/53/show/Products/notes/index.htt#008},
  tags = {protocol},
  researchr = {https://researchr.org/publication/DawsKN02},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {66},
  number = {2},
  pages = {104-119},
}

@article{NormanPPW09,
  title = {Model Checking Probabilistic and Stochastic Extensions of the pi-Calculus},
  author = {Gethin J. Norman and Catuscia Palamidessi and David Parker and Peng Wu 0002},
  year = {2009},
  doi = {10.1109/TSE.2008.77},
  url = {http://dx.doi.org/10.1109/TSE.2008.77},
  tags = {model checking, meta-model, Meta-Environment},
  researchr = {https://researchr.org/publication/NormanPPW09},
  cites = {0},
  citedby = {0},
  journal = {TSE},
  volume = {35},
  number = {2},
  pages = {209-223},
}

@inproceedings{KwiatkowskaNPS03,
  title = {Performance Analysis of Probabilistic Timed Automata Using Digital Clocks},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and David Parker and Jeremy Sproston},
  year = {2003},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2791&spage=105},
  tags = {analysis},
  researchr = {https://researchr.org/publication/KwiatkowskaNPS03},
  cites = {0},
  citedby = {0},
  pages = {105-120},
  booktitle = {formats},
}

@article{KwiatkowskaNP05,
  title = {Probabilistic model checking in practice: case studies with PRISM},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and David Parker},
  year = {2005},
  doi = {10.1145/1059816.1059820},
  url = {http://doi.acm.org/10.1145/1059816.1059820},
  tags = {case study, model checking, meta-model, Meta-Environment},
  researchr = {https://researchr.org/publication/KwiatkowskaNP05},
  cites = {0},
  citedby = {0},
  journal = {sigmetrics},
  volume = {32},
  number = {4},
  pages = {16-21},
}

@inproceedings{KwiatkowskaNP06:1,
  title = {Symmetry Reduction for Probabilistic Model Checking},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and David Parker},
  year = {2006},
  doi = {10.1007/11817963_23},
  url = {http://dx.doi.org/10.1007/11817963_23},
  tags = {model checking, meta-model, Meta-Environment},
  researchr = {https://researchr.org/publication/KwiatkowskaNP06%3A1},
  cites = {0},
  citedby = {0},
  pages = {234-248},
  booktitle = {cav},
}

@inproceedings{DuflotKNP04,
  title = {A Formal Analysis of Bluetooth Device Discovery},
  author = {Marie Duflot and Marta Z. Kwiatkowska and Gethin J. Norman and David Parker},
  year = {2004},
  tags = {discovery, analysis},
  researchr = {https://researchr.org/publication/DuflotKNP04},
  cites = {0},
  citedby = {0},
  pages = {268-275},
  booktitle = {ISoLA},
}

@article{KattenbeltKNP08,
  title = {Game-Based Probabilistic Predicate Abstraction in PRISM},
  author = {Mark Kattenbelt and Marta Z. Kwiatkowska and Gethin J. Norman and David Parker},
  year = {2008},
  doi = {10.1016/j.entcs.2008.11.016},
  url = {http://dx.doi.org/10.1016/j.entcs.2008.11.016},
  tags = {rule-based, abstraction},
  researchr = {https://researchr.org/publication/KattenbeltKNP08},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {220},
  number = {3},
  pages = {5-21},
}

@article{BaierKN99,
  title = {Computing Probability Bounds for Linear Time Formulas over Concurrent Probabilistic Systems},
  author = {Christel Baier and Marta Z. Kwiatkowska and Gethin J. Norman},
  year = {1999},
  url = {http://www.elsevier.com/gej-ng/31/29/23/46/23/show/Products/notes/index.htt#003},
  researchr = {https://researchr.org/publication/BaierKN99},
  cites = {0},
  citedby = {0},
  journal = {ENTCS},
  volume = {22},
  pages = {29},
}

@inproceedings{KwiatkowskaN96,
  title = {Probabilistic Metric Semantics for a Simple Language with Recursion},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman},
  year = {1996},
  tags = {semantics},
  researchr = {https://researchr.org/publication/KwiatkowskaN96},
  cites = {0},
  citedby = {0},
  pages = {419-430},
  booktitle = {mfcs},
}

@article{KwiatkowskaNPS06,
  title = {Performance analysis of probabilistic timed automata using digital clocks},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and David Parker and Jeremy Sproston},
  year = {2006},
  doi = {10.1007/s10703-006-0005-2},
  url = {http://dx.doi.org/10.1007/s10703-006-0005-2},
  tags = {analysis},
  researchr = {https://researchr.org/publication/KwiatkowskaNPS06},
  cites = {0},
  citedby = {0},
  journal = {fmsd},
  volume = {29},
  number = {1},
  pages = {33-78},
}

@inproceedings{NormanPPW07,
  title = {Model checking the probabilistic pi-calculus},
  author = {Gethin J. Norman and Catuscia Palamidessi and David Parker and Peng Wu 0002},
  year = {2007},
  doi = {10.1109/QEST.2007.27},
  url = {http://doi.ieeecomputersociety.org/10.1109/QEST.2007.27},
  tags = {model checking, meta-model, Meta-Environment},
  researchr = {https://researchr.org/publication/NormanPPW07},
  cites = {0},
  citedby = {0},
  pages = {169-178},
  booktitle = {qest},
}

@inproceedings{RoyPNA08,
  title = {Symbolic Magnifying Lens Abstraction in Markov Decision Processes},
  author = {Pritam Roy and David Parker and Gethin J. Norman and Luca de Alfaro},
  year = {2008},
  doi = {10.1109/QEST.2008.41},
  url = {http://dx.doi.org/10.1109/QEST.2008.41},
  tags = {Markov, abstraction},
  researchr = {https://researchr.org/publication/RoyPNA08},
  cites = {0},
  citedby = {0},
  pages = {103-112},
  booktitle = {qest},
}

@article{YounesKNP06,
  title = {Numerical vs. statistical probabilistic model checking},
  author = {Håkan L. S. Younes and Marta Z. Kwiatkowska and Gethin J. Norman and David Parker},
  year = {2006},
  doi = {10.1007/s10009-005-0187-8},
  url = {http://dx.doi.org/10.1007/s10009-005-0187-8},
  tags = {model checking, meta-model, Meta-Environment},
  researchr = {https://researchr.org/publication/YounesKNP06},
  cites = {0},
  citedby = {0},
  journal = {STTT},
  volume = {8},
  number = {3},
  pages = {216-228},
}

@article{KwiatkowskaNS03,
  title = {Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention Protocol},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and Jeremy Sproston},
  year = {2003},
  doi = {10.1007/s001650300007},
  url = {http://dx.doi.org/10.1007/s001650300007},
  tags = {model checking, meta-model, protocol, Meta-Environment},
  researchr = {https://researchr.org/publication/KwiatkowskaNS03},
  cites = {0},
  citedby = {0},
  journal = {fac},
  volume = {14},
  number = {3},
  pages = {295-318},
}

@inproceedings{KwiatkowskaNP04,
  title = {PRISM 2.0: A Tool for Probabilistic Model Checking},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and David Parker},
  year = {2004},
  url = {http://csdl.computer.org/comp/proceedings/qest/2004/2185/00/21850322abs.htm},
  tags = {model checking, meta-model, Meta-Environment},
  researchr = {https://researchr.org/publication/KwiatkowskaNP04},
  cites = {0},
  citedby = {0},
  pages = {322-323},
  booktitle = {qest},
}

@inproceedings{GrosserNBCKP06,
  title = {On Reduction Criteria for Probabilistic Reward Models},
  author = {Marcus Größer and Gethin J. Norman and Christel Baier and Frank Ciesinski and Marta Z. Kwiatkowska and David Parker},
  year = {2006},
  doi = {10.1007/11944836_29},
  url = {http://dx.doi.org/10.1007/11944836_29},
  tags = {meta-model, Meta-Environment},
  researchr = {https://researchr.org/publication/GrosserNBCKP06},
  cites = {0},
  citedby = {0},
  pages = {309-320},
  booktitle = {fsttcs},
}

@inproceedings{NormanS02,
  title = {Analysis of Probabilistic Contract Signing},
  author = {Gethin J. Norman and Vitaly Shmatikov},
  year = {2002},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2629&spage=81},
  tags = {contracts, analysis},
  researchr = {https://researchr.org/publication/NormanS02},
  cites = {0},
  citedby = {0},
  pages = {81-96},
  booktitle = {fasec},
}

@inproceedings{KwiatkowskaNP02:1,
  title = {PRISM: Probabilistic Symbolic Model Checker},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and David Parker},
  year = {2002},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2324&spage=0200},
  tags = {meta-model, Meta-Environment},
  researchr = {https://researchr.org/publication/KwiatkowskaNP02%3A1},
  cites = {0},
  citedby = {0},
  pages = {200-204},
  booktitle = {cpe},
}

@inproceedings{KwiatkowskaNP07,
  title = {Stochastic Model Checking},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and David Parker},
  year = {2007},
  doi = {10.1007/978-3-540-72522-0_6},
  url = {http://dx.doi.org/10.1007/978-3-540-72522-0_6},
  tags = {model checking, meta-model, Meta-Environment, meta-objects},
  researchr = {https://researchr.org/publication/KwiatkowskaNP07},
  cites = {0},
  citedby = {0},
  pages = {220-270},
  booktitle = {sfm},
}

@inproceedings{KwiatkowskaNP02:0,
  title = {Model Checking CSL until Formulae with Random Time Bounds},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and António Pacheco},
  year = {2002},
  url = {http://link.springer.de/link/service/series/0558/bibs/2399/23990152.htm},
  tags = {model checking, meta-model, Meta-Environment},
  researchr = {https://researchr.org/publication/KwiatkowskaNP02%3A0},
  cites = {0},
  citedby = {0},
  pages = {152-168},
  booktitle = {papm},
}

@inproceedings{ChatzikokolakisNP09,
  title = {Bisimulation for Demonic Schedulers},
  author = {Konstantinos Chatzikokolakis and Gethin J. Norman and David Parker},
  year = {2009},
  doi = {10.1007/978-3-642-00596-1_23},
  url = {http://dx.doi.org/10.1007/978-3-642-00596-1_23},
  researchr = {https://researchr.org/publication/ChatzikokolakisNP09},
  cites = {0},
  citedby = {0},
  pages = {318-332},
  booktitle = {fossacs},
}

@inproceedings{JurdzinskiKNT09,
  title = {Concavely-Priced Probabilistic Timed Automata},
  author = {Marcin Jurdzinski and Marta Z. Kwiatkowska and Gethin J. Norman and Ashutosh Trivedi},
  year = {2009},
  doi = {10.1007/978-3-642-04081-8_28},
  url = {http://dx.doi.org/10.1007/978-3-642-04081-8_28},
  researchr = {https://researchr.org/publication/JurdzinskiKNT09},
  cites = {0},
  citedby = {0},
  pages = {415-430},
  booktitle = {concur},
}

@article{HermannsKNPS03,
  title = {On the use of MTBDDs for performability analysis and verification of stochastic systems},
  author = {Holger Hermanns and Marta Z. Kwiatkowska and Gethin J. Norman and David Parker and Markus Siegle},
  year = {2003},
  doi = {10.1016/S1567-8326(02)00066-8},
  url = {http://dx.doi.org/10.1016/S1567-8326(02)00066-8},
  tags = {analysis},
  researchr = {https://researchr.org/publication/HermannsKNPS03},
  cites = {0},
  citedby = {0},
  journal = {jlp},
  volume = {56},
  number = {1-2},
  pages = {23-67},
}

@inproceedings{KwiatkowskaNS02,
  title = {Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and Jeremy Sproston},
  year = {2002},
  url = {http://link.springer.de/link/service/series/0558/bibs/2399/23990169.htm},
  tags = {model checking, meta-model, protocol, Meta-Environment},
  researchr = {https://researchr.org/publication/KwiatkowskaNS02},
  cites = {0},
  citedby = {0},
  pages = {169-187},
  booktitle = {papm},
}

@inproceedings{KwiatkowskaNP09,
  title = {Stochastic Games for Verification of Probabilistic Timed Automata},
  author = {Marta Z. Kwiatkowska and Gethin J. Norman and David Parker},
  year = {2009},
  doi = {10.1007/978-3-642-04368-0_17},
  url = {http://dx.doi.org/10.1007/978-3-642-04368-0_17},
  researchr = {https://researchr.org/publication/KwiatkowskaNP09},
  cites = {0},
  citedby = {0},
  pages = {212-227},
  booktitle = {formats},
}

@inproceedings{NormanPKS04,
  title = {Evaluating the Reliability of Defect-Tolerant Architectures for Nanotechnology with Probabilistic Model Checking},
  author = {Gethin J. Norman and David Parker and Marta Z. Kwiatkowska and Sandeep K. Shukla},
  year = {2004},
  url = {http://csdl.computer.org/comp/proceedings/vlsid/2004/2072/00/20720907abs.htm},
  tags = {model checking, meta-model, architecture, Meta-Environment, reliability},
  researchr = {https://researchr.org/publication/NormanPKS04},
  cites = {0},
  citedby = {0},
  pages = {907},
  booktitle = {vlsid},
}