Verification and control of partially observable probabilistic real-time systems

DOI10.1007/978-3-319-22975-1_16zbMATH Open1465.68182arXiv1506.06419OpenAlexW2097415230MaRDI QIDQ2945599FDOQ2945599

Authors:

Publication date: 14 September 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Abstract: We propose automated techniques for the verification and control of probabilistic real-time systems that are only partially observable. To formally model such systems, we define an extension of probabilistic timed automata in which local states are partially visible to an observer or controller. We give a probabilistic temporal logic that can express a range of quantitative properties of these models, relating to the probability of an event's occurrence or the expected value of a reward measure. We then propose techniques to either verify that such a property holds or to synthesise a controller for the model which makes it true. Our approach is based on an integer discretisation of the model's dense-time behaviour and a grid-based abstraction of the uncountable belief space induced by partial observability. The latter is necessarily approximate since the underlying problem is undecidable, however we show how both lower and upper bounds on numerical results can be generated. We illustrate the effectiveness of the approach by implementing it in the PRISM model checker and applying it to several case studies, from the domains of computer security and task scheduling.

Full work available at URL: https://arxiv.org/abs/1506.06419

Recommendations

• Verification and control of partially observable probabilistic systems
• Automatic verification of real-time systems with discrete probability distributions.
• Timed control with partial observability.
• scientific article; zbMATH DE number 1507207
• scientific article; zbMATH DE number 1759607

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems involving computers (process control, etc.) (93C83) Computer security (68M25)

Cites Work

• A theory of timed automata
• On the undecidability of probabilistic planning and related stochastic optimization problems
• What good are digital clocks?
• What is decidable about partially observable Markov decision processes with omega-regular objectives
• On Decision Problems for Probabilistic Büchi Automata
• Model checking for probabilistic timed automata
• Performance analysis of probabilistic timed automata using digital clocks
• Partial-observation stochastic games, how to win when belief fails
• Timed control with partial observability.
• Title not available (Why is that?)
• Verification and control of partially observable probabilistic real-time systems
• A course in triangulations for solving equations with deformations
• Automatic analysis of a non-repudiation protocol
• Title not available (Why is that?)
• Computationally Feasible Bounds for Partially Observed Markov Decision Processes
• Template-based controller synthesis for timed systems
• Timed Control with Observation Based and Stuttering Invariant Strategies
• Verification of partial-information probabilistic systems using counterexample-guided refinements
• Information and Communications Security

Cited In (10)

• Polynomial-time probabilistic observability analysis of sampled-data piecewise affine systems
• Data-driven verification of stochastic linear systems with signal temporal logic constraints
• Finite state approximation for verification of partially observable stochastic hybrid systems
• Verification and control of partially observable probabilistic real-time systems
• Verification and control of partially observable probabilistic systems
• Probabilistic reach-avoid problems in nondeterministic systems with time-varying targets and obstacles
• Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives
• Verification of partial-information probabilistic systems using counterexample-guided refinements
• Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata
• Deductive controller synthesis for probabilistic hyperproperties

Uses Software

• PRISM
• POMDP

This page was built for publication: Verification and control of partially observable probabilistic real-time systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2945599)