@article(AILS12,
 author       = {Luca Aceto and Anna Ing{\'{o}}lfsd{\'{o}}ttir and Paul Blain Levy and Joshua Sack},
 year         = {2012},
 title        = {Characteristic formulae for fixed-point semantics: a general framework},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {22},
 number       = {2},
 pages        = {125--173},
 doi          = {$10.1017/S0960129511000375$},
)
@article(ABG04,
 author       = {Alessandro Aldini and Mario Bravetti and Roberto Gorrieri},
 year         = {2004},
 title        = {A process-algebraic approach for the analysis of probabilistic noninterference},
 journal      = {Journal of Computer Security},
 volume       = {12},
 number       = {2},
 pages        = {191--245},
 doi          = {$10.3233$/JCS-$2004$-$12202$},
 url          = {http://content.iospress.com/articles/journal-of-computer-security/jcs198},
)
@inproceedings(ABdPGHW02,
 author       = {Alessandro Aldini and Mario Bravetti and Alessandra Di Pierro and Roberto Gorrieri and Chris Hankin and Herbert Wiklicky},
 year         = {2002},
 title        = {Two Formal Approaches for Approximating Noninterference Properties},
 booktitle    = {{FOSAD} 2001/2002},
 pages        = {1--43},
 doi          = {$10.1007/978$-$3$-$540$-$24631$-$2\_1$},
)
@inproceedings(AFS04,
 author       = {Luca de Alfaro and Marco Faella and Mari{\"{e}}lle Stoelinga},
 year         = {2004},
 title        = {Linear and Branching Metrics for Quantitative Transition Systems},
 booktitle    = {Proc.~{ICALP} 2004},
 pages        = {97--109},
 doi          = {$10.1007/978$-$3$-$540$-$27836$-$8\_11$},
)
@inproceedings(AHM03,
 author       = {Luca de Alfaro and Thomas A. Henzinger and Rupak Majumdar},
 year         = {2003},
 title        = {Discounting the Future in Systems Theory},
 booktitle    = {Proc.~{ICALP} 2003},
 pages        = {1022--1037},
 doi          = {$10.1007/3$-$540$-$45061$-$0\_79$},
)
@article(AMRS08,
 author       = {Luca de Alfaro and Rupak Majumdar and Vishwanath Raman and Mari{\"{e}}lle Stoelinga},
 year         = {2008},
 title        = {Game Refinement Relations and Metrics},
 journal      = {Logical Methods in Computer Science},
 volume       = {4},
 number       = {3},
 doi          = {$10.2168/$LMCS-$4(3:7)2008$},
)
@article(BBLM14,
 author       = {Giorgio Bacci and Giovanni Bacci and Kim G. Larsen and Radu Mardare},
 year         = {2014},
 title        = {Topologies of Stochastic Markov Models: Computational Aspects},
 journal      = {CoRR},
 volume       = {abs/1403.6032},
 url          = {http://arxiv.org/abs/1403.6032},
)
@phdthesis(B98,
 author       = {Christel Baier},
 year         = {1998},
 title        = {On Algorithmic Verification Methods for Probabilistic Systems},
 school       = {Uviversit{\"{a}}t Mannheim},
)
@article(BdNL15,
 author       = {Marco Bernardo and {De Nicola}, Rocco and Michele Loreti},
 year         = {2015},
 title        = {Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes},
 journal      = {Acta Inf.},
 volume       = {52},
 number       = {1},
 pages        = {61--106},
 doi          = {$10.1007/s00236$-$014$-$0210$-$1$},
)
@article(BFvG04,
 author       = {Bard Bloom and Wan J. Fokkink and Rob J. van Glabbeek},
 year         = {2004},
 title        = {Precongruence formats for decorated trace semantics},
 journal      = {{ACM} Trans.~Comput.~Log.},
 volume       = {5},
 number       = {1},
 pages        = {26--78},
 doi          = {$10.1145/963927.963929$},
)
@article(vB12,
 author       = {Franck van Breugel},
 year         = {2012},
 title        = {On behavioural pseudometrics and closure ordinals},
 journal      = {Inf.~Process.~Lett.},
 volume       = {112},
 number       = {19},
 pages        = {715--718},
 doi          = {$10.1016/$j.ipl.$2012.06.019$},
)
@inproceedings(BW01b,
 author       = {Franck van Breugel and James Worrell},
 year         = {2001},
 title        = {An Algorithm for Quantitative Verification of Probabilistic Transition Systems},
 booktitle    = {Proc.~{CONCUR} 2001},
 pages        = {336--350},
 doi          = {$10.1007/3$-$540$-$44685$-$0\_23$},
)
@article(BW05,
 author       = {Franck van Breugel and James Worrell},
 year         = {2005},
 title        = {A behavioural pseudometric for probabilistic transition systems},
 journal      = {Theor.~Comput.~Sci.},
 volume       = {331},
 number       = {1},
 pages        = {115--142},
 doi          = {$10.1016/$j.tcs.$2004.09.035$},
)
@inproceedings(CGT16b,
 author       = {Valentina Castiglioni and Daniel Gebler and Simone Tini},
 year         = {2016},
 title        = {Modal Decomposition on Nondeterministic Probabilistic Processes},
 booktitle    = {Proc.~{CONCUR} 2016},
 series       = {LIPIcs},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
 doi          = {$10.4230$/LIPIcs.CONCUR.$2016.36$},
)
@inproceedings(CGPX14,
 author       = {Konstantinos Chatzikokolakis and Daniel Gebler and Catuscia Palamidessi and Lili Xu},
 year         = {2014},
 title        = {Generalized Bisimulation Metrics},
 booktitle    = {Proc.~{CONCUR} 2014},
 pages        = {32--46},
 doi          = {$10.1007/978$-$3$-$662$-$44584$-$6\_4$},
)
@inproceedings(CE81,
 author       = {Edmund M. Clarke and E. Allen Emerson},
 year         = {1981},
 title        = {Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic},
 booktitle    = {Proc.~Logics of Programs},
 pages        = {52--71},
 doi          = {$10.1007/$BFb$0025774$},
)
@article(dATW12,
 author       = {Pedro R. D'Argenio and Pedro S{\'{a}}nchez Terraf and Nicol{\'{a}}s Wolovick},
 year         = {2012},
 title        = {Bisimulations for non-deterministic labelled Markov processes},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {22},
 number       = {1},
 pages        = {43--68},
 doi          = {$10.1017/S0960129511000454$},
)
@article(DCPP06,
 author       = {Yuxin Deng and Tom Chothia and Catuscia Palamidessi and Jun Pang},
 year         = {2006},
 title        = {Metrics for Action-labelled Quantitative Transition Systems},
 journal      = {Electr.~Notes Theor.~Comput.~Sci.},
 volume       = {153},
 number       = {2},
 pages        = {79--96},
 doi          = {$10.1016/$j.entcs.$2005.10.033$},
)
@article(DD11,
 author       = {Yuxin Deng and Wenjie Du},
 year         = {2011},
 title        = {Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation},
 journal      = {CoRR},
 volume       = {abs/1103.4577},
 url          = {http://arxiv.org/abs/1103.4577},
)
@article(DDG15,
 author       = {Yuxin Deng and Wenjie Du and Daniel Gebler},
 year         = {2015},
 title        = {Modal Characterisations of Behavioural Pseudometrics},
 journal      = {CoRR},
 volume       = {abs/1509.03391},
 url          = {http://arxiv.org/abs/1509.03391},
)
@inproceedings(DFdL15,
 author       = {Yuxin Deng and Yuan Feng and Ugo Dal Lago},
 year         = {2015},
 title        = {On Coinduction and Quantum Lambda Calculi},
 booktitle    = {Proc.~{CONCUR} 2015},
 pages        = {427--440},
 doi          = {$10.4230/$LIPIcs.CONCUR.$2015.427$},
)
@inproceedings(DvG10,
 author       = {Yuxin Deng and Rob J. van Glabbeek},
 year         = {2010},
 title        = {Characterising Probabilistic Processes Logically - (Extended Abstract)},
 booktitle    = {Proc.~LPAR-17},
 pages        = {278--293},
 doi          = {$10.1007/978$-$3$-$642$-$16242$-$8\_20$},
)
@article(DvGHM08,
 author       = {Yuxin Deng and Rob J. van Glabbeek and Matthew Hennessy and Carroll Morgan},
 year         = {2008},
 title        = {Characterising Testing Preorders for Finite Probabilistic Processes},
 journal      = {Logical Methods in Computer Science},
 volume       = {4},
 number       = {4},
 doi          = {$10.2168/$LMCS-$4(4:4)2008$},
)
@article(DEP02,
 author       = {Josee Desharnais and Abbas Edalat and Prakash Panangaden},
 year         = {2002},
 title        = {Bisimulation for Labelled Markov Processes},
 journal      = {Inf.~Comput.},
 volume       = {179},
 number       = {2},
 pages        = {163--193},
 doi          = {$10.1006/$inco.$2001.2962$},
)
@article(DGJP04,
 author       = {Josee Desharnais and Vineet Gupta and Radha Jagadeesan and Prakash Panangaden},
 year         = {2004},
 title        = {Metrics for labelled Markov processes},
 journal      = {Theor.~Comput.~Sci.},
 volume       = {318},
 number       = {3},
 pages        = {323--354},
 doi          = {$10.1016/$j.tcs.$2003.09.013$},
)
@inproceedings(DJGP02,
 author       = {Josee Desharnais and Radha Jagadeesan and Vineet Gupta and Prakash Panangaden},
 year         = {2002},
 title        = {The Metric Analogue of Weak Bisimulation for Probabilistic Processes},
 booktitle    = {Proc.~LICS 2002},
 pages        = {413--422},
 doi          = {$10.1109/$LICS$.2002.1029849$},
)
@incollection(E90,
 author       = {E. Allen Emerson},
 year         = {1990},
 title        = {Temporal and Modal Logic},
 booktitle    = {Handbook of Theoretical Computer Science, Volume {B:} Formal Models and Sematics {(B)}},
 pages        = {995--1072},
)
@article(FL14,
 author       = {Uli Fahrenberg and Axel Legay},
 year         = {2014},
 title        = {The quantitative linear-time-branching-time spectrum},
 journal      = {Theor.~Comput.~Sci.},
 volume       = {538},
 pages        = {54--69},
 doi          = {$10.1016/$j.tcs.$2013.07.030$},
)
@inproceedings(FZ14,
 author       = {Yuan Feng and Lijun Zhang},
 year         = {2014},
 title        = {When Equivalence and Bisimulation Join Forces in Probabilistic Automata},
 booktitle    = {Proc.~{FM} 2014},
 pages        = {247--262},
 doi          = {$10.1007/978$-$3$-$319$-$06410$-$9\_18$},
)
@article(FvG16,
 author       = {Wan J. Fokkink and Robert J. van Glabbeek},
 year         = {2016},
 title        = {Divide and Congruence {II:} From Decomposition of Modal Formulas to Preservation of Delay and Weak Bisimilarity},
 journal      = {CoRR},
 volume       = {abs/1604.07530},
)
@article(FvGW06,
 author       = {Wan J. Fokkink and Robert J. van Glabbeek and Paulien de Wind},
 year         = {2006},
 title        = {Compositionality of {H}ennessy-{M}ilner logic by structural operational semantics},
 journal      = {Theoret.~Comput.~Sci.},
 volume       = {354},
 number       = {3},
 pages        = {421--440},
 doi          = {$10.1016$/j.tcs.$2005.11.035$},
)
@article(FvGW12,
 author       = {Wan J. Fokkink and Robert J. van Glabbeek and Paulien de Wind},
 year         = {2012},
 title        = {Divide and congruence: From decomposition of modal formulas to preservation of branching and {$\eta$}-bisimilarity},
 journal      = {Inf.~Comput.},
 volume       = {214},
 pages        = {59--85},
 doi          = {$10.1016$/j.ic.$2011.10.011$},
)
@inproceedings(GF12,
 author       = {Daniel Gebler and Wan J. Fokkink},
 year         = {2012},
 title        = {Compositionality of Probabilistic Hennessy-Milner Logic through Structural Operational Semantics},
 booktitle    = {Proc.~{CONCUR} 2012},
 pages        = {395--409},
 doi          = {$10.1007/978$-$3$-$642$-$32940$-$1\_28$},
)
@inproceedings(GLT15,
 author       = {Daniel Gebler and Kim G. Larsen and Simone Tini},
 year         = {2015},
 title        = {Compositional Metric Reasoning with Probabilistic Process Calculi},
 booktitle    = {Proc.~FoSSaCS 2015},
 pages        = {230--245},
 doi          = {$10.1007/978$-$3$-$662$-$46678$-$0\_15$},
)
@article(GLT16,
 author       = {Daniel Gebler and Kim G. Larsen and Simone Tini},
 year         = {2016},
 title        = {Compositional metric reasoning with Probabilistic Process Calculi},
 journal      = {Logical Methods in Computer Science},
)
@inproceedings(GT14,
 author       = {Daniel Gebler and Simone Tini},
 year         = {2014},
 title        = {Fixed-point Characterization of Compositionality Properties of Probabilistic Processes Combinators},
 booktitle    = {Proc.~{EXPRESS/SOS} 2014},
 pages        = {63--78},
 doi          = {$10.4204/$EPTCS.$160.7$},
)
@inproceedings(GT15,
 author       = {Daniel Gebler and Simone Tini},
 year         = {2015},
 title        = {{SOS} Specifications of Probabilistic Systems by Uniformly Continuous Operators},
 booktitle    = {Proc.~{CONCUR} 2015},
 pages        = {155--168},
 doi          = {$10.4230/$LIPIcs.CONCUR.$2015.155$},
)
@inproceedings(GJS90,
 author       = {Alessandro Giacalone and Chi-Chang Jou and Scott A. Smolka},
 year         = {1990},
 title        = {Algebraic Reasoning for Probabilistic Concurrent Systems},
 booktitle    = {Proc.~IFIP Work, Conf.~on Programming, Concepts and Methods},
 pages        = {443--458},
)
@article(GS86a,
 author       = {Susanne Graf and Joseph Sifakis},
 year         = {1986},
 title        = {A Modal Characterization of Observational Congruence on Finite Terms of {CCS}},
 journal      = {Information and Control},
 volume       = {68},
 number       = {1-3},
 pages        = {125--145},
 doi          = {$10.1016/S0019$-$9958(86)80031$-$6$},
)
@article(H12,
 author       = {Matthew Hennessy},
 year         = {2012},
 title        = {Exploring Probabilistic Bisimulations, part {I}},
 journal      = {Formal Asp.~Comput.},
 volume       = {24},
 number       = {4-6},
 pages        = {749--768},
 doi          = {$10.1007/s00165$-$012$-$0242$-$7$},
)
@article(HM85,
 author       = {Matthew Hennessy and Robin Milner},
 year         = {1985},
 title        = {Algebraic laws for nondeterminism and concurrency},
 journal      = {J.~Assoc.~Comput.~Mach.},
 volume       = {32},
 pages        = {137--161},
 doi          = {$10.1145/2455.2460$},
)
@inproceedings(HKK14,
 author       = {Holger Hermanns and Jan Krc{\'{a}}l and Kret{\'{\i}}nsk{\'{y}}, Jan},
 year         = {2014},
 title        = {Probabilistic Bisimulation: Naturally on Distributions},
 booktitle    = {Proc.~{CONCUR} 2014},
 pages        = {249--265},
 doi          = {$10.1007/978$-$3$-$662$-$44584$-$6\_18$},
)
@article(HPSWZ11,
 author       = {Holger Hermanns and Augusto Parma and Roberto Segala and Bj{\"{o}}rn Wachter and Lijun Zhang},
 year         = {2011},
 title        = {Probabilistic Logical Characterization},
 journal      = {Inf.~Comput.},
 volume       = {209},
 number       = {2},
 pages        = {154--172},
 doi          = {$10.1016/$j.ic.$2010.11.024$},
)
@article(K42,
 author       = {Leonid V. Kantorovich},
 year         = {1942},
 title        = {On the Transfer of Masses},
 journal      = {Doklady Akademii Nauk},
 volume       = {37},
 number       = {2},
 pages        = {227--229},
 note         = {Original article in Russian, translation in Management Science, $5: 1-4 (1959)$},
)
@article(K76,
 author       = {Robert M. Keller},
 year         = {1976},
 title        = {Formal Verification of Parallel Programs},
 journal      = {Commun.~{ACM}},
 volume       = {19},
 number       = {7},
 pages        = {371--384},
 doi          = {$10.1145/360248.360251$},
)
@inproceedings(KN96,
 author       = {Marta Z. Kwiatkowska and Gethin Norman},
 year         = {1996},
 title        = {Probabilistic Metric Semantics for a Simple Language with Recursion},
 booktitle    = {Proc.~MFCS'96},
 pages        = {419--430},
 doi          = {$10.1007/3$-$540$-$61550$-$4\_167$},
)
@incollection(LT05,
 author       = {Ruggero Lanotte and Simone Tini},
 year         = {2005},
 title        = {Probabilistic Congruence for Semistochastic Generative Processes},
 booktitle    = {Proc.~FoSSaCS'05},
 series       = {LNCS},
 volume       = {3441},
 publisher    = {Springer},
 pages        = {63--78},
 doi          = {$10.1007/978$-$3$-$540$-$31982$-$5\_4$},
)
@article(LT09,
 author       = {Ruggero Lanotte and Simone Tini},
 year         = {2009},
 title        = {Probabilistic Bisimulation as a Congruence},
 journal      = {ACM TOCL},
 volume       = {10},
 pages        = {1--48},
 doi          = {$10.1145/1462179.1462181$},
)
@article(L90,
 author       = {Kim G. Larsen},
 year         = {1990},
 title        = {Proof Systems for Satisfiability in Hennessy-Milner Logic with Recursion},
 journal      = {Theor.~Comput.~Sci.},
 volume       = {72},
 number       = {2{\&}3},
 pages        = {265--288},
 doi          = {$10.1016/0304$-$3975(90)90038$-J},
)
@inproceedings(LMP12,
 author       = {Kim G. Larsen and Radu Mardare and Prakash Panangaden},
 year         = {2012},
 title        = {Taking It to the Limit: Approximate Reasoning for Markov Processes},
 booktitle    = {Proc.~{MFCS} 2012},
 pages        = {681--692},
 doi          = {$10.1007/978$-$3$-$642$-$32589$-$2\_59$},
)
@article(LS91,
 author       = {Kim G. Larsen and Arne Skou},
 year         = {1991},
 title        = {Bisimulation through Probabilistic Testing},
 journal      = {Inf.~Comput.},
 volume       = {94},
 number       = {1},
 pages        = {1--28},
 doi          = {$10.1016/0890$-$5401(91)90030$-$6$},
)
@article(MCL12,
 author       = {Radu Mardare and Luca Cardelli and Kim G. Larsen},
 year         = {2012},
 title        = {Continuous Markovian Logics - Axiomatization and Quantified Metatheory},
 journal      = {Logical Methods in Computer Science},
 volume       = {8},
 number       = {4},
 doi          = {$10.2168/$LMCS-$8(4:19)2012$},
)
@inproceedings(P81,
 author       = {David M. R. Park},
 year         = {1981},
 title        = {Concurrency and automata of infinite sequences.},
 booktitle    = {Proc.~$5^{th}$ GI Conference},
 series       = {LNCS},
 volume       = {104},
 publisher    = {Springer},
 pages        = {167--183},
 doi          = {$10.1007/$BFb$0017309$},
)
@inproceedings(PS07,
 author       = {Augusto Parma and Roberto Segala},
 year         = {2007},
 title        = {Logical Characterizations of Bisimulations for Discrete Probabilistic Systems},
 booktitle    = {Proc.~FoSSaCS 2007},
 pages        = {287--301},
 doi          = {$10.1007/978$-$3$-$540$-$71389$-$0\_21$},
)
@inproceedings(dPHW03,
 author       = {Alessandra Di Pierro and Chris Hankin and Herbert Wiklicky},
 year         = {2003},
 title        = {Quantitative Relations and Approximate Process Equivalences},
 booktitle    = {Proc.~{CONCUR} 2003},
 pages        = {498--512},
 doi          = {$10.1007/978$-$3$-$540$-$45187$-$7\_33$},
)
@inproceedings(SZ12,
 author       = {Joshua Sack and Lijun Zhang},
 year         = {2012},
 title        = {A General Framework for Probabilistic Characterizing Formulae},
 booktitle    = {Proc.~{VMCAI} 2012},
 pages        = {396--411},
 doi          = {$10.1007/978$-$3$-$642$-$27940$-$9_26$},
)
@phdthesis(S95,
 author       = {Roberto Segala},
 year         = {1995},
 title        = {Modeling and Verification of Randomized Distributed Real-Time Systems},
 school       = {MIT},
)
@article(SL95,
 author       = {Roberto Segala and Nancy A. Lynch},
 year         = {1995},
 title        = {Probabilistic Simulations for Probabilistic Processes},
 journal      = {Nord.~J.~Comput.},
 volume       = {2},
 number       = {2},
 pages        = {250--273},
)
@inproceedings(T08,
 author       = {Simone Tini},
 year         = {2008},
 title        = {Non Expansive epsilon-Bisimulations},
 booktitle    = {Proc.~{AMAST} 2008},
 pages        = {362--376},
 doi          = {$10.1007/978$-$3$-$540$-$79980$-$1\_27$},
)
@article(T10,
 author       = {Simone Tini},
 year         = {2010},
 title        = {Non-expansive epsilon-bisimulations for probabilistic processes},
 journal      = {Theor.~Comput.~Sci.},
 volume       = {411},
 number       = {22-24},
 pages        = {2202--2222},
 doi          = {$10.1016/$j.tcs.$2010.01.027$},
)
@book(Vil08,
 author       = {C\'edric Villani},
 year         = {2009},
 title        = {Optimal transport: old and new},
 publisher    = {Springer},
 doi          = {$10.1007/978$-$3$-$540$-$71050$-$9$},
)