包邮概率进程语义-(英文版)

1  introduction  1.1  background  1.2  synopsis  references2  mathematical preliminaries  2.1  lattice theory  2.2  induction and coinduction  2.3  topological spaces  2.4  metric spaces  2.5  probability spaces  2.6  linear programming  references3  probabilistic bisimulation  3.1  introduction  3.2  probabilistic labelled transition systems  3.3  lifting relations  3.4  justifving the lifting operation    3.4.1  justification by the kantorovich memc    3.4.2  justification by network flow  3.5  probabilistic bisimulation  3.6  logical characterisation    3.6.1  an adequate logic    3.6.2  an expressive logic  3.7  metric characterisation  3.8  algorithmic characterisation    3.8.1  a partition refinement algorithm    3.8.2  an“on—the—fly”algorithm  3.9  bibliographic notes    3.9.1  probabilistic models    3.9.2  probabilistic bisimulation  references4  probabilistic testine semantics  4.1  a general testing framework  4.2  testing probabilistic processes  4.3  bounded continuity  4.4  reward testing    4.4.1  a geometric property    4.4.2  nonnegative rewards  4.5  extremal reward testing  4.6  extremal reward testing versus resolution—based reward testing    4.6.1  must testing    4.6.2  may testing  4.7  vector—based testing versus scalar testin~  4.8  bibliographic notes  references5  testing finite probabilistic processes  5.1  introduction  5.2  the language pcsp    5.2.1  the syntax    5.2.2  the operational semantics    5.2.3  the precedence of probabilistic choice    5.2.4  graphical representation of pcsp processes    5.2.5  testing pcsp processes  5.3  counterexamples  5.4  must versus may testing  5.5  forward and failure simulation    5.5.1  the simulation preorders    5.5.2  the simulation preorders are precongruences    5.5.3  simulations are sound for testing preorders  5.6  a modal logic  5.7  characteristic tests  5.8  equational theories  5.9  inequational theories  5.10  comoletenes  5.11  bibliographic notes    5.11.1  probabilistic equivalences    5.11.2  probabilistic simulations  references6  testing finitary probabilistic processes  6.1  introduction  6.2  the language rpcsp  6.3  a general definition of weak derivations    6.3.1  lifting relations    6.3.2  weak transitions    6.3.3  properties of weak transitions  6.4  testing rpcsp processes    6.4.1  testing with extremal derivatives    6.4.2  comparison with resolution—based testing  6.5  generatinz weak derivatives in a finitary plts    6.5.1  finite generability    6.5.2  realising payoffs    6.5.3  conseauences  6.6  the failure simulation preorder    6.6.1  two equivalent definitions and their rationale    6.6.2  a simple failure similarity for finitary processes    6.6.3  precongruence    6.6.4  soundness  6.7  failure simulation is complete for must testing    6.7.1  inductive characterisatior    6.7.2  the modal logic    6.7.3  characteristic tests for formulae  6.8  simulations and may testing    6.8.1  soundness    6.8.2  completeness  6.9  real—reward testing  6.10  summary  references7  weak probabilistic bisimulation  7.1  introduction  7.2  a simple bisimulation  7.3  compositionality  7.4  reduction barbed congruence  7.5  bibliographic notes  referencesindex