Abstract

The aim of the paper is to sketch some solutions that arose along the work on Logic of Strict Processes . Three main topics are discussed: negation based on implication constructed in intuitionistic fashion; satisfiability in multimodal contexts and a proposal of a first order semantics for Dynamic Logic of Strict Processes . The system of DLSP differs from the original LSP in using the set of contexts, which are treated as ordered sets of formulas. The interpretation of a context is a transition system, which is constructed solely of simple processes. After the set of non-allowed processes is constructed, the negation of molecular formula can be understood as a set o processes that, when combined with processes associated with a non-negated formula, produce non-allowed processes. Satisfiablity in a transition system is defined by a special modal operator [φ]φ which is true only when the relation of metaimplication between φ and φ holds. In conclusion the author briefly reviews first order system based on DLSP and points to several open problems waiting for further investigation