A General Framework for Probabilistic Characterizing Formulae

DOI10.1007/978-3-642-27940-9_26zbMath1326.68176OpenAlexW180602404MaRDI QIDQ2891432

Joshua Sack, Li-jun Zhang

Publication date: 15 June 2012

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-27940-9_26

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Probability and inductive logic (03B48) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (7)

Computing Behavioral Relations for Probabilistic Concurrent Systems ⋮ CryptHOL: game-based proofs in higher-order logic ⋮ Explainability of probabilistic bisimilarity distances for labelled Markov chains ⋮ Unnamed Item ⋮ Logical characterization of branching metrics for nondeterministic probabilistic transition systems ⋮ Probabilistic Functions and Cryptographic Oracles in Higher Order Logic ⋮ A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory

Cites Work

• Unnamed Item
• Unnamed Item
• The Max-Flow Min-Cut theorem for countable networks
• Probabilistic logical characterization
• On the use of MTBDDs for performability analysis and verification of stochastic systems.
• Deciding bisimilarity and similarity for probabilistic processes.
• Weak bisimulation is sound and complete for pCTL\(^*\)
• Finite models constructed from canonical formulas
• A lattice-theoretical fixpoint theorem and its applications
• Characteristic formulae for fixed-point semantics: a general framework
• Model checking of probabilistic and nondeterministic systems
• Partial Order Reduction for Probabilistic Systems: A Revision for Distributed Schedulers
• A Compositional Semantics for Dynamic Fault Trees in Terms of Interactive Markov Chains
• Characterising Probabilistic Processes Logically
• Logical Characterizations of Bisimulations for Discrete Probabilistic Systems

This page was built for publication: A General Framework for Probabilistic Characterizing Formulae