@book(Abrial96B,
 author       = {Jean-Raymond Abrial},
 year         = {1996},
 title        = {The B Book: Assigning Programs to Meanings},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511624162},
)
@incollection(ASB95,
 author       = {Adnan Aziz and Vigyan Singhal and Felice Balarin and RobertK. Brayton and Sangiovanni-Vincentelli, AlbertoL.},
 year         = {1995},
 title        = {It usually works: The temporal logic of stochastic systems},
 editor       = {Pierre Wolper},
 booktitle    = {Computer Aided Verification},
 series       = {Lecture Notes in Computer Science},
 volume       = {939},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {155--165},
 doi          = {10.1007/3-540-60045-0\unhbox\voidb@x \vbox{\hrule width0.5em}48},
)
@book(BaierKatoen:2008,
 author       = {C. {Baier} and J. P. {Katoen}},
 year         = {2008},
 title        = {Principles of Model Checking},
 publisher    = {MIT Press},
 address      = {New York},
)
@incollection(CA82,
 author       = {Edmund M. Clarke and E.Allen Emerson},
 year         = {1982},
 title        = {Design and synthesis of synchronization skeletons using branching time temporal logic},
 editor       = {Dexter Kozen},
 booktitle    = {Logics of Programs},
 series       = {Lecture Notes in Computer Science},
 volume       = {131},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {52--71},
 doi          = {10.1007/BFb0025774},
)
@incollection(Clarke:StatisticalMC,
 author       = {Edmund M. Clarke and Paolo Zuliani},
 year         = {2011},
 title        = {Statistical Model Checking for Cyber-Physical Systems},
 editor       = {Tevfik Bultan and Pao-Ann Hsiung},
 booktitle    = {Automated Technology for Verification and Analysis},
 series       = {Lecture Notes in Computer Science},
 volume       = {6996},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {1--12},
 doi          = {10.1007/978-3-642-24372-1\unhbox\voidb@x \vbox{\hrule width0.5em}1},
)
@article(EshuisJansenWieringa02RequirementsStatecharts,
 author       = {Rik Eshuis and David N. Jansen and Roel Wieringa},
 year         = {2002},
 title        = {Requirements-Level Semantics and Model Checking of Object-Oriented Statecharts},
 journal      = {Requirements Engineering},
 volume       = {V7},
 number       = {4},
 pages        = {243--263},
 doi          = {10.1007/s007660200019},
)
@phdthesis(Fruth11,
 author       = {Matthias Fruth},
 year         = {2011},
 title        = {Formal Methods for the Analysis of Wireless Network Protocols},
 school       = {University of Oxford},
)
@inproceedings(HK04,
 author       = {David Harel and Hillel Kugler},
 year         = {2004},
 title        = {The Rhapsody Semantics of Statecharts (or, On the Executable Core of the UML)},
 editor       = {Hartmut Ehrig and Werner Damm and J{\"o}rg Desel and Gro{\ss}e-Rhode, Martin and Wolfgang Reif and Eckehard Schnieder and Engelbert Westk{\"a}mper},
 booktitle    = {Integration of Software Specification Techniques for Applications in Engineering},
 series       = {Lecture Notes in Computer Science},
 volume       = {3147},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {325--354},
 doi          = {10.1007/978-3-540-27863-4\unhbox\voidb@x \vbox{\hrule width0.5em}19},
)
@article(HN96,
 author       = {David Harel and Amnon Naamad},
 year         = {1996},
 title        = {The STATEMATE Semantics of Statecharts},
 journal      = {ACM Trans. Softw. Eng. Methodol.},
 volume       = {5},
 number       = {4},
 pages        = {293--333},
 doi          = {10.1145/235321.235322},
)
@phdthesis(Jansen03StatechartExtensions,
 author       = {D. N. Jansen},
 year         = {2003},
 title        = {Extensions of Statecharts with Probability, Time, and Stochastic Timing},
 school       = {University of Twente},
 address      = {Enschede},
 url          = {http://doc.utwente.nl/58230/},
)
@inproceedings(JansenHermannsKatoen02ProbabilisticUMLStatecharts,
 author       = {D.N. Jansen and H. Hermanns and J.P. Katoen},
 year         = {2002},
 title        = {A probabilistic extension of {UML} statecharts: Specification and Verification.},
 editor       = {W. Damm and E.-R. Olderog},
 booktitle    = {Formal Techniques in Real-Time and Fault-Tolerant Systems},
 series       = {Lecture Notes in Computer Science 2469},
 publisher    = {Springer},
 address      = {Oldenburg, Germany},
 pages        = {355--374},
 doi          = {10.1007/3-540-45739-9},
)
@inproceedings(PTAKwiatkowska:2009,
 author       = {Marta Kwiatkowska and Gethin Norman and David Parker},
 year         = {2009},
 title        = {Stochastic Games for Verification of Probabilistic Timed Automata},
 booktitle    = {Proceedings of the 7th International Conference on Formal Modeling and Analysis of Timed Systems},
 series       = {FORMATS '09},
 publisher    = {Springer-Verlag},
 address      = {Berlin, Heidelberg},
 pages        = {212--227},
 doi          = {10.1007/978-3-642-04368-0\unhbox\voidb@x \vbox{\hrule width0.5em}17},
)
@inproceedings(KwiatkowskaNormanParker11PRISM4,
 author       = {Marta Kwiatkowska and Gethin Norman and David Parker},
 year         = {2011},
 title        = {PRISM 4.0: Verification of Probabilistic Real-Time Systems},
 editor       = {Ganesh Gopalakrishnan and Shaz Qadeer},
 booktitle    = {Computer Aided Verification},
 series       = {Lecture Notes in Computer Science},
 volume       = {6806},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {585--591},
 doi          = {10.1007/978-3-642-22110-1\unhbox\voidb@x \vbox{\hrule width0.5em}47},
)
@article(KNSW04,
 author       = {Marta Kwiatkowska and Gethin Norman and Jeremy Sproston and Fuzhi Wang},
 year         = {2007},
 title        = {Symbolic model checking for probabilistic timed automata},
 journal      = {Information and Computation},
 volume       = {205},
 number       = {7},
 pages        = {1027 -- 1077},
 doi          = {10.1016/j.ic.2007.01.004},
 url          = {http://www.sciencedirect.com/science/article/pii/S0890540107000077},
)
@article(KNPS06,
 author       = {Marta Z. Kwiatkowska and Gethin Norman and David Parker and Jeremy Sproston},
 year         = {2006},
 title        = {Performance analysis of probabilistic timed automata using digital clocks},
 journal      = {Formal Methods in System Design},
 volume       = {29},
 number       = {1},
 pages        = {33--78},
 doi          = {10.1007/s10703-006-0005-2},
)
@inproceedings(LeitnerFischerLeue11QuantUM,
 author       = {Leitner-Fischer, Florian and Stefan Leue},
 year         = {2011},
 title        = {QuantUM: Quantitative Safety Analysis of UML Models},
 editor       = {Mieke Massink and Gethin Norman},
 booktitle    = {{\rm Proceedings Ninth Workshop on} Quantitative Aspects of Programming Languages, {\rm Saarbr\"ucken, Germany, April 1-3, 2011}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {57},
 publisher    = {Open Publishing Association},
 pages        = {16--30},
 doi          = {10.4204/EPTCS.57.2},
)
@inproceedings(luttgen:00,
 author       = {Gerald L{\"o}ttgen and Michael Mendler},
 year         = {2000},
 title        = {Fully-Abstract Statecharts Semantics via Intuitionistic Kripke Models.},
 booktitle    = {ICALP},
 series       = {Lecture Notes in Computer Science},
 volume       = {1853},
 publisher    = {Springer},
 pages        = {163--174},
 doi          = {10.1007/3-540-45022-X\unhbox\voidb@x \vbox{\hrule width0.5em}14},
 url          = {http://dblp.uni-trier.de/db/conf/icalp/icalp2000.html#LuttgenM00},
)
@article(MorganMcIverSeidel96ProbabilisticPredicateTransformers,
 author       = {Carroll Morgan and Annabelle McIver and Karen Seidel},
 year         = {1996},
 title        = {Probabilistic Predicate Transformers},
 journal      = {ACM Trans. Program. Lang. Syst.},
 volume       = {18},
 number       = {3},
 pages        = {325--353},
 doi          = {10.1145/229542.229547},
 url          = {http://doi.acm.org.libaccess.lib.mcmaster.ca/10.1145/229542.229547},
)
@techreport(NokovicSekerinski10Interrrogator,
 author       = {Bojan Nokovic and Emil Sekerinski},
 year         = {2010},
 title        = {Analysis of Interrogator-tag Communication Protocols},
 type         = {{SQRL} Report},
 number       = {60},
 institution  = {McMaster University},
)
@inproceedings(NokovicSekerinski13pState,
 author       = {Bojan Nokovic and Emil Sekerinski},
 year         = {2013},
 title        = {p{S}tate: A probabilistic statecharts translator},
 booktitle    = {Embedded Computing (MECO), 2013 2nd Mediterranean Conference on},
 pages        = {29--32},
 doi          = {10.1109/MECO.2013.6601339},
)
@inproceedings(NokovicSekerinski14pCharts,
 author       = {Bojan Nokovic and Emil Sekerinski},
 year         = {2014},
 title        = {Verification and Code Generation for Timed Transitions in p{C}harts},
 booktitle    = {Proceedings of the 2014 International C* Conference on Computer Science~\#38; Software Engineering},
 series       = {C3S2E '14},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {3:1--3:10},
 doi          = {10.1145/2641483.2641522},
)
@article(NormanParkerSproston12ModelCheckingPTA,
 author       = {G. Norman and D. Parker and J. Sproston},
 year         = {2012},
 title        = {Model checking for probabilistic timed automata},
 journal      = {Formal Methods in System Design},
 pages        = {1--27},
 doi          = {10.1007/s10703-012-0177-x},
)
@mastersthesis(Oldenkamp07,
 author       = {H.A. {Oldenkamp}},
 year         = {2007},
 title        = {Probabilistic model checking : a comparison of tools},
 school       = {University of Twente},
 url          = {http://essay.utwente.nl/591/},
)
@phdthesis(Segala95RandomizedDistributedRealTime,
 author       = {Roberto Segala},
 year         = {1995},
 title        = {Modelling and Verification of Randomized Distributed Real Time Systems},
 type         = {{Ph.D. thesis, Technical Report MIT/LCS/TR-676}},
 school       = {Massachusetts Institute of Technology},
 url          = {http://profs.sci.univr.it/~segala/www/phd.html},
)
@inproceedings(Seker08,
 author       = {E. Sekerinski},
 year         = {2008},
 title        = {Verifying Statecharts with State Invariants},
 booktitle    = {Proceedings of the 13th IEEE International Conference on on Engineering of Complex Computer Systems},
 publisher    = {IEEE Computer Society},
 address      = {Washington, DC, USA},
 pages        = {7--14},
 doi          = {10.1109/ICECCS.2008.40},
)
@article(SZ01,
 author       = {E. Sekerinski and R. Zurob},
 year         = {2001},
 title        = {{iState}: A Statechart Translator},
 journal      = {In M. Gogolla and C. Kobryn, editors UML 2001 - The Unified Modeling Language, 4th International Conference, {Lecture Notes in Computer Science 2185, pages 376-390, Toronto, Canada}},
 doi          = {10.1007/3-540-45441-1\unhbox\voidb@x \vbox{\hrule width0.5em}28},
)
@incollection(Sekerinski09StateInvariants,
 author       = {Emil Sekerinski},
 year         = {2009},
 title        = {Design Verification with State Invariants},
 editor       = {Kevin Lano},
 booktitle    = {UML 2 Semantics and Applications},
 publisher    = {John Wiley \& Sons},
 pages        = {317--347},
 doi          = {10.1002/9780470522622},
)
@article(ZhaoYangXieLiu00QuantitativeUMLStateDiagrams,
 author       = {Yefei Zhao and Zongyuan Yang and Jinkui Xie and Qiang Liu},
 year         = {2010},
 title        = {Quantitative Analysis of System Based on Extended {UML} State Diagrams and Probabilistic Model Checking},
 journal      = {{JSW}},
 volume       = {5},
 number       = {7},
 pages        = {793--800},
 doi          = {10.4304/jsw.5.7.793-800},
)