An In-Depth Investigation of Interval Temporal Logic Model Checking with Regular Expressions

摘要: In the last years, model checking (MC) problem for interval temporal logic (ITL) has received an increasing attention as a viable alternative to traditional (point-based) MC, which can be recovered special case. Most results have been obtained by imposing suitable restrictions on labeling. this paper, we overcome such limitations using regular expressions define behavior of proposition letters over intervals in terms component states. We first prove that MC Halpern and Shoham’s ITL (HS), extended with expressions, is decidable. Then, show formulas large class HS fragments, namely, all fragments featuring (a subset of) modalities Allen’s relations meets, met-by, starts, started-by, checked polynomial working space (MC these turns out PSPACE-complete).