Probabilistic model checking of systems with ranged probabilities
AssigneeNEC Laboratories America, Inc.
InventorsParasara Sridhar Duggirala, Khalil Ghorbal, Franjo Ivancic, Vineet Kahlon, Aarti Gupta
Life of this patent
Estimating the term…
Abstract
Systems and methods for model checking of live systems are shown that include learning an interval discrete-time Markov chain (IDTMC) model of a deployed system from system logs; and checking the IDTMC model with a processor to determine a probability of violating one or more probabilistic safety properties. Checking the IDTMC model includes calculating a linear part exactly using affine arithmetic; and over-approximating a non-linear part using interval arithmetic.
Claims10
A method for model checking of deployed systems, comprising:
- learning an interval discrete-time Markov chain (IDTMC) model of a deployed system from system logs;
- and
- checking the IDTMC model with a processor to determine a probability of violating one or more probabilistic safety properties, comprising:
- splitting the probability into a linear part and a non-linear part;
- and
- calculating the linear part exactly using affine arithmetic;
- and
- over-approximating the non-linear part using interval arithmetic.
A system for model checking of deployed systems, comprising:
- a model learning module configured to learn an interval discrete-time Markov chain (IDTMC) model of a deployed system from system logs;
- and
- a processor configured to check the IDTMC model to determine a probability of violating one or more probabilistic safety properties, wherein the probability is split into a linear part and a non-linear part, comprising:
- an affine module configured to calculate a linear part exactly using affine arithmetic;
- and
- an interval module configured to over-approximate a non-linear part using interval arithmetic.
Dependencies are inferred from the claim text.