Interval Change-Point Detection for Runtime Probabilistic Model Checking.

Xingyu Zhao Radu Calinescu Simos Gerasimou Valentin Robu David Flynn

Published in: ASE (2020)

Keyphrases

model checking
change point detection
temporal logic
change point
formal specification
finite state
temporal properties
formal verification

model checker
non stationary
computation tree logic
probabilistic model
automated verification
reachability analysis
verification method
formal methods

outlier detection
symbolic model checking
epistemic logic
process algebra
pspace complete
bounded model checking
concurrent systems
timed automata

transition systems
linear temporal logic
normalized maximum likelihood
bayesian networks
knowledge discovery
deterministic finite automaton
asynchronous circuits