Vladimir V. Rybakov
Department of Computing and Mathematics, Manchester Metropolitan University, UK

Our paper studies a special temporal logic TL^Z_DU 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^Z_DU. Our principal result is found algorithm which checks if any given formula is true in TL^Z_DU (which implies that TL^Z_DU is decidable, and the satisfiability problem for is TL^Z_DU solvable). We also enumerate several interesting open problems within suggested technique.