Temporal Logic TL ^Z_ {DU} Modeling Local and Global Discovery with Logical Uncertainty

Our paper studies a special temporal logic TL_DU^Z combining operations of the linear temporal logic LTL, the operation for discovery (variations of chance discovery - CD) and operation for logical uncertainty. We distinguish local and global discovery in the temporal logic approach. Main aim of our paper is to construct a logical framework for modeling logical laws connecting chance discovery (CD), temporal logical operations and the logical operation of uncertainty. We aim to solve questions of satisfiability and decidability for TL_DU^Z. Our principal result is found algorithm which checks if any given formula is true in TL_DU^Z (which implies that TL_DU^Z is decidable, and the satisfiability problem for TL_DU^Z is solvable). We also enumerate several interesting open problems within suggested technique.