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

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, On Quantitative Modelling and Verification of DNA Walker Circuits Using Stochastic Petri Nets, SOS specifications for uniformly continuous operators, Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination, Model checking quantum Markov chains, Branching-time model-checking of probabilistic pushdown automata, Twenty years of rewriting logic, A survey on temporal logics for specifying and verifying real-time systems, Approximating labelled Markov processes, Model checking differentially private properties, Minimal probabilistic P systems for modelling ecological systems, Model-checking large structured Markov chains., Algebraic theory of probabilistic processes., Probabilistic verification of Herman's self-stabilisation algorithm, Verification and control of partially observable probabilistic systems, Markov chains and Markov decision processes in Isabelle/HOL, Probabilistic contracts: a compositional reasoning methodology for the design of systems with stochastic and/or non-deterministic aspects, Minimization of probabilistic models of programs, Maximal traces and path-based coalgebraic temporal logics, Coalgebraic semantics of modal logics: an overview, Consistency and refinement for interval Markov chains, Three-valued abstraction for probabilistic systems, Computing branching distances with quantitative games, Symbolic checking of fuzzy CTL on fuzzy program graph, A propositional linear time logic with time flow isomorphic to \(\omega^2\), Generating counterexamples for quantitative safety specifications in probabilistic B, Reachability in recursive Markov decision processes, Where logic and agents meet, Multi-scale verification of distributed synchronisation, Improving active Mealy machine learning for protocol conformance testing, Deciding bisimilarity and similarity for probabilistic processes., Sublogics of a branching time logic of robustness, Towards general axiomatizations for bisimilarity and trace semantics, Quantitative verification of Kalman filters, Automaton-ABC: a statistical method to estimate the probability of spatio-temporal properties for parametric Markov population models, Automatic verification of competitive stochastic systems, Preface to the special issue on probabilistic model checking, Analyzing probabilistic pushdown automata, Model checking for probabilistic timed automata, Bayesian statistical model checking with application to Stateflow/Simulink verification, Unnamed Item, Probabilistic verification and approximation, Model checking fuzzy computation tree logic, Quantitative Kleene coalgebras, Probabilization of logics: completeness and decidability, Deciding probabilistic bisimilarity over infinite-state probabilistic systems, Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes, Performability assessment by model checking of Markov reward models, The well-designed logical robot: learning and experience from observations to the Situation Calculus, Probabilistic divide \& congruence: branching bisimilarity, Constraint Markov chains, An AGM-style belief revision mechanism for probabilistic spatio-temporal logics, Model checking expected time and expected reward formulae with random time bounds, A modular approach to defining and characterising notions of simulation, Logical characterization of branching metrics for nondeterministic probabilistic transition systems, Model checking mobile stochastic logic, Statistical probabilistic model checking with a focus on time-bounded properties, Computation tree measurement language (CTML), Probabilistic mobile ambients, Refinement Sensitive Formal Semantics of State Machines With Persistent Choice, CEGAR for compositional analysis of qualitative properties in Markov decision processes, Temporal logic with recursion, A linear process-algebraic format with data for probabilistic automata, Probabilistic model checking of biological systems with uncertain kinetic rates, Raiders of the lost equivalence: probabilistic branching bisimilarity, A note on the attractor-property of infinite-state Markov chains, Towards light-weight probabilistic model checking, On finite-state approximants for probabilistic computation tree logic, Quantitative \(\mu\)-calculus and CTL defined over constraint semirings, On probabilistic timed automata., Weak Probabilistic Anonymity, On the verification of qualitative properties of probabilistic processes under fairness constraints., Exogenous Probabilistic Computation Tree Logic, Testing preorders for probabilistic processes can be characterized by simulations, Automatic verification of real-time systems with discrete probability distributions., Quantitative program logic and expected time bounds in probabilistic distributed algorithms., Modular Games for Coalgebraic Fixed Point Logics, Model checking for entanglement swapping, eBCSgen 2.0: modelling and analysis of regulated rule-based systems, 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

Uses Software

Cites Work