Parametric probabilistic transition systems for system design and analysis

DOI10.1007/s00165-006-0015-2zbMath1111.68084OpenAlexW2000865099MaRDI QIDQ877158

Angelo Troina, Ruggero Lanotte, Andrea Maggiolo-Schettini

Publication date: 19 April 2007

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-006-0015-2

zbMATH Keywords

ReachabilityParametersDiscrete-time Markov chainsProbabilistic non-repudiation protocol

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

Parameter Synthesis Algorithms for Parametric Interval Markov Chains, Formal abstraction and synthesis of parametric stochastic processes, Stochastic equivalence for performance analysis of concurrent systems in dtsiPBC, Fine-tuning the odds in Bayesian networks, Gradient-descent for randomized controllers under partial observability, The complexity of reachability in parametric Markov decision processes, Unnamed Item, Multi-objective Parameter Synthesis in Probabilistic Hybrid Systems, Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination, Parameter-Independent Strategies for pMDPs via POMDPs, POMDP controllers with optimal budget, Interval Markov Decision Processes with Continuous Action-Spaces, Unnamed Item, Model Repair for Probabilistic Systems, On the Complexity of Reachability in Parametric Markov Decision Processes, An extension of the inverse method to probabilistic timed automata, Finding provably optimal Markov chains, Probabilistic Model Checking of Biological Systems with Uncertain Kinetic Rates, Compositional weak metrics for group key update, System design of stochastic models using robustness of temporal properties

Uses Software

• HyTech
• Uppaal

Cites Work

• Metrics for labelled Markov processes
• Weak bisimulation for probabilistic timed automata
• A decomposition theorem for probabilistic transition systems
• The dining cryptographers problem: Unconditional sender and recipient untraceability
• Bisimulation through probabilistic testing
• On the computational complexity and geometry of the first-order theory of the reals. I: Introduction. Preliminaries. The geometry of semi-algebraic sets. The decision problem for the existential theory of the reals
• A theory of timed automata
• A logic for reasoning about time and reliability
• Composition and behaviors of probabilistic I/O automata
• Approximating labelled Markov processes
• HyTech: A model checker for hybrid systems
• Axiomatizing probabilistic processes: ACP with generative probabilities
• On the verification of qualitative properties of probabilistic processes under fairness constraints.
• Model checking of probabilistic and nondeterministic systems
• Probability with Martingales
• Parametric real-time reasoning
• Theoretical Aspects of Computing - ICTAC 2004
• 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