A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences

DOI10.1016/j.ic.2013.02.004zbMath1358.68210OpenAlexW2146187895WikidataQ124439082 ScholiaQ124439082MaRDI QIDQ384933

Michele Loreti, Marco Bernardo, Rocco De Nicola

Publication date: 29 November 2013

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2013.02.004

zbMATH Keywords

testing equivalencesbisimulation equivalencesdiscrete-/continuous-time Markov chainsdiscrete-/continuous-time Markov decision processeslabeled transition systemstrace equivalences

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (15)

Timed process calculi with deterministic or stochastic delays: commuting between durational and durationless actions ⋮ A general SOS theory for the specification of probabilistic transition systems ⋮ Equivalences for fluid stochastic Petri nets ⋮ \textsc{ULTraS} at work: compositionality metaresults for bisimulation and trace semantics ⋮ A framework to measure the robustness of programs in the unpredictable environment ⋮ Back to the format: a survey on SOS for probabilistic processes ⋮ Towards general axiomatizations for bisimilarity and trace semantics ⋮ Structural operational semantics for non-deterministic processes with quantitative aspects ⋮ Model-based testing of probabilistic systems ⋮ Relating strong behavioral equivalences for processes with nondeterminism and probabilities ⋮ Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes ⋮ Best-by-simulations: a framework for comparing efficiency of reconfigurable architectures on workloads with deadlines ⋮ Group-by-Group Probabilistic Bisimilarities and Their Logical Characterizations ⋮ Logical characterization of fluid equivalences ⋮ How adaptive and reliable is your program?

Uses Software

• PEPA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Bisimulation and simulation algorithms on probabilistic transition systems by abstract interpretation
• Observation equivalence as a testing equivalence
• Probabilistic logical characterization
• Probabilistic communicating processes
• Probabilistic and prioritized models of timed CSP
• Interactive Markov chains. And the quest for quantified quality
• Branching bisimulation congruence for probabilistic systems
• Equivalence notions and model minimization in Markov decision processes
• Axiomatizations for probabilistic finite-state behaviors
• CCS expressions, finite state processes, and three problems of equivalence
• Optimal state-space lumping in Markov chains
• A complete inference system for a class of regular behaviours
• Extensional equivalences for transition systems
• A tutorial on EMPA: A theory of concurrent processes with nondeterminism, priorities, probabilities and time
• Bisimulation through probabilistic testing
• A complete axiomatisation for observational congruence of finite-state behaviours
• A theory of timed automata
• Processes with probabilities, priority and time
• Testing equivalences for processes
• Probabilistic models for the guarded command language
• Algebraic theory of probabilistic and nondeterministic processes.
• Algebraic theory of probabilistic processes.
• Testing preorders for probabilistic processes can be characterized by simulations
• Automatic verification of real-time systems with discrete probability distributions.
• Performance measure sensitive congruences for Markovian process algebras
• Discrete time generative-reactive probabilistic processes with different advancing speeds
• Testing preorders for probabilistic processes.
• Absolute versus relative time in process algebras.
• A structural approach to operational semantics
• Reactive, generative, and stratified models of probabilistic processes
• Axiomatizing probabilistic processes: ACP with generative probabilities
• Exploring probabilistic bisimulations. I
• Deciding bisimilarity and similarity for probabilistic processes.
• Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes
• Weak bisimulation is sound and complete for pCTL\(^*\)
• Refinement-oriented probability for CSP
• Testing equivalence as a bisimulation equivalence
• Non-bisimulation-based Markovian behavioral equivalences
• Comparative branching-time semantics for Markov chains
• Branching bisimulation for probabilistic systems: characteristics and decidability
• Bisimulation for labelled Markov processes
• Finite state Markovian decision processes
• Revisiting Trace and Testing Equivalences for Nondeterministic and Probabilistic Processes
• Efficient Modelling and Generation of Markov Automata
• Equational Axioms for Probabilistic Bisimilarity
• Bisimulations Meet PCTL Equivalences for Probabilistic Automata
• Testing Finitary Probabilistic Processes
• Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes
• Game Refinement Relations and Metrics
• A testing scenario for probabilistic processes
• Retaining the Probabilities in Probabilistic Testing Theory
• Characterising Testing Preorders for Finite Probabilistic Processes
• Process algebra for synchronous communication
• A Theory of Communicating Sequential Processes
• Algebraic laws for nondeterminism and concurrency
• Acceptance trees
• Three Partition Refinement Algorithms
• A Polynomial-Time Algorithm for the Equivalence of Probabilistic Automata
• Formal verification of parallel programs
• Branching time and abstraction in bisimulation semantics
• Rate-Based Transition Systems for Stochastic Process Calculi
• Validation of Stochastic Systems
• A uniform definition of stochastic process calculi
• Probabilistic automata
• Continuous-time probabilistic automata
• Scalar Outcomes Suffice for Finitary Probabilistic Testing
• CONCUR 2003 - Concurrency Theory
• Testing probabilistic automata

This page was built for publication: A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences