A General Framework for Probabilistic Characterizing Formulae

DOI10.1007/978-3-642-27940-9_26zbMath1326.68176MaRDI 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

68Q45: Formal languages and automata

03B48: Probability and inductive logic

68Q60: Specification and verification (program logics, model checking, etc.)

68Q87: Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)

Related Items

Unnamed Item, CryptHOL: game-based proofs in higher-order logic, Logical characterization of branching metrics for nondeterministic probabilistic transition systems, Probabilistic Functions and Cryptographic Oracles in Higher Order Logic, Computing Behavioral Relations for Probabilistic Concurrent Systems

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