Abstract

Logic-based formalisms have been used to approach the most intriguing open problems of computer science related to modelling computational processes and analyzing computational complexity. In many approaches, non-determinism plays a significant role, and the effects of it are difficult to analyze. In this talk, I will describe an algebraic approach to modelling non-determinism. The algebra formalizes non-deterministic computations in a semi-deterministic way, here non-determinism is confined to the atomic level. The algebra has in an equivalent form of a linear-time (as opposite to branching-time) Dynamic Logic. A crucial role is played by a new kind of choice functions that are history-dependent. Solving computational problems corresponds to generating strategies in a one-player game.