|
Abstract : |
abstract. We consider frames that can be defined by polynomials over states and transitions. States are elements from the natural numbers with pairing, and (state-)transitions are labeled with actions from some finite set. We study a connection with process algebra: pointing a frame by distinguishing either two states that function as a root and a tail, respectively, implements a terminating process. Only selecting a root can be used to model a non-terminating process. This implies that frame properties can be investigated with process algebraic means. Providing further structure on frames by inserting propositions at the states, gives a basic "framework " for Floyd Hoare logic, or a modal logic with modalities 2a for all actions a considered. Note: This paper will be published in: Modal Logic and Process algebra, Alban, |
