A logic for reasoning about time and reliability

DOI10.1007/BF01211866zbMath0820.68113OpenAlexW2005998857MaRDI QIDQ1343864

Publication date: 9 February 1995

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

Full work available at URL: https://doi.org/10.1007/bf01211866

zbMATH Keywords

modal logic Markov chains model checking

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (only showing first 100 items - show all)

Robust Control for Dynamical Systems with Non-Gaussian Noise via Formal Abstractions ⋮ Scenario-Based Verification of Uncertain MDPs ⋮ Deep Statistical Model Checking ⋮ Baire Category Quantifier in Monadic Second Order Logic ⋮ Model Checking Probabilistic Systems ⋮ Model Checking of Biological Systems ⋮ Validation of Decentralised Smart Contracts Through Game Theory and Formal Methods ⋮ Deriving Syntax and Axioms for Quantitative Regular Behaviours ⋮ Counterexamples in Probabilistic LTL Model Checking for Markov Chains ⋮ Strict Divergence for Probabilistic Timed Automata ⋮ Unnamed Item ⋮ Model Checking Linear-Time Properties of Probabilistic Systems ⋮ Symbolic model checking for probabilistic processes ⋮ Logical Characterizations of Behavioral Relations on Transition Systems of Probability Distributions ⋮ Expressiveness and succinctness of a logic of robustness ⋮ ExplicitPRISMSymm: Symmetry Reduction Technique for Explicit Models in PRISM ⋮ Model checking, synthesis, and learning ⋮ Quantitative analysis of interval Markov chains ⋮ On counting propositional logic and Wagner's hierarchy ⋮ HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties ⋮ Action and State Based Computation Tree Measurement Language and Algorithms ⋮ Model Checking for Safe Navigation Among Humans ⋮ Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference ⋮ A specification logic for programs in the probabilistic guarded command language ⋮ Satisfiability of quantitative probabilistic CTL: rise to the challenge ⋮ Sound approximate and asymptotic probabilistic bisimulations for PCTL ⋮ Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic ⋮ Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking ⋮ A Markovian model for the spread of the SARS-CoV-2 virus ⋮ \textsf{PFL}: a probabilistic logic for fault trees ⋮ QMaude: quantitative specification and verification in rewriting logic ⋮ Probabilistic CEGAR ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives ⋮ Compositional bisimulation metric reasoning with Probabilistic Process Calculi ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Cognitive Reasoning and Trust in Human-Robot Interactions ⋮ Unnamed Item ⋮ Statistical Verification of Probabilistic Properties with Unbounded Until ⋮ Model Repair for Probabilistic Systems ⋮ Model Checking Exact Cost for Attack Scenarios ⋮ MODEL THEORY OF MEASURE SPACES AND PROBABILITY LOGIC ⋮ Temporal Logic with Recursion. ⋮ Model checking with probabilistic tabled logic programming ⋮ Quantitative Verification of Stochastic Regular Expressions ⋮ Model Checking Quantitative Linear Time Logic ⋮ Probabilistic Logic over Paths ⋮ Energy-Utility Analysis for Resilient Systems Using Probabilistic Model Checking ⋮ Pebble Weighted Automata and Weighted Logics ⋮ Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations ⋮ Quantifying opacity ⋮ Approximate Verification of the Symbolic Dynamics of Markov Chains ⋮ Branching-Time Model-Checking of Probabilistic Pushdown Automata ⋮ The satisfiability problem for a quantitative fragment of PCTL ⋮ Meanings of Model Checking ⋮ Model checking for a class of weighted automata ⋮ Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata ⋮ Survey on Directed Model Checking ⋮ A weakness measure for GR(1) formulae ⋮ A weakness measure for GR(1) formulae ⋮ Model-Checking ω-Regular Properties of Interval Markov Chains ⋮ Bisimulations Meet PCTL Equivalences for Probabilistic Automata ⋮ A Spectrum of Behavioral Relations over LTSs on Probability Distributions ⋮ Weighted versus Probabilistic Logics ⋮ Verifying Team Formation Protocols with Probabilistic Model Checking ⋮ OBLIGATION BLACKWELL GAMES AND P-AUTOMATA ⋮ Extended Stochastic Petri Nets for Model-Based Design of Wetlab Experiments ⋮ Probabilistic Model Checking of Biological Systems with Uncertain Kinetic Rates ⋮ LTL Model Checking of Time-Inhomogeneous Markov Chains ⋮ Statistical Model Checking Using Perfect Simulation ⋮ Multi-valued Verification of Strategic Ability ⋮ A Multi-level Refinement Approach for Structural Synthesis of Optimal Probabilistic Models ⋮ Compositional weak metrics for group key update ⋮ Non-determinism and Probabilities in Timed Concurrent Constraint Programming ⋮ Bisimulation and Simulation Relations for Markov Chains ⋮ Probabilistic Temporal Logics ⋮ Belief and truth in hypothesised behaviours ⋮ A weak semantic approach to bisimulation metrics in models with nondeterminism and continuous state spaces ⋮ Not all bugs are created equal, but robust reachability can tell the difference ⋮ A stochastic games framework for verification and control of discrete time stochastic hybrid systems ⋮ Reasoning about probabilistic sequential programs ⋮ Symbolic model checking for probabilistic timed automata ⋮ The satisfiability problem for a quantitative fragment of PCTL ⋮ An efficient algorithm to determine probabilistic bisimulation ⋮ Trust evidence logic ⋮ Nondeterministic probabilistic Petri net -- a new method to study qualitative and quantitative behaviors of system ⋮ Automatic verification of concurrent stochastic systems ⋮ Modelling accuracy and trustworthiness of explaining agents ⋮ Performance analysis of probabilistic timed automata using digital clocks ⋮ Means-end relations and a measure of efficacy ⋮ Comparative branching-time semantics for Markov chains ⋮ Generic Infinite Traces and Path-Based Coalgebraic Temporal Logics ⋮ Formal analysis of PIN block attacks ⋮ A Tutorial on Interactive Markov Chains ⋮ On Abstraction of Probabilistic Systems ⋮ Computing Behavioral Relations for Probabilistic Concurrent Systems ⋮ Parametric probabilistic transition systems for system design and analysis ⋮ Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes

Uses Software

Cites Work

This page was built for publication: A logic for reasoning about time and reliability