Characteristic Formulae for Processes with Divergence

B. Steffen, A. Ingolfsdottir

	   Characteristic formulae have been introduced by Graf and
	   Sifakis to relate equational reasoning about processes to
	   reasoning in a modal logic, and therefore to allow proofs about
	   processes to be carried out in a logical framework. This work,
	   which concerned {\em finite} processes and bisimulation-like
	   {\em equivalences}, has later on been extended to {\em finite
	   state} processes and further equivalences.  Based upon an
	   intuitionistic understanding of Hennessy-Milner logic (HML)
	   with mutual recursion, we extend these results to cover
	   bisimulation-like {\em preorders}, which are sensitive to
	   liveness properties. This demonstrates the expressive power of
	   intuitionistically interpreted HML with mutual recursion, and
	   it builds the theoretical basis for a uniform and efficient
	   method to {\em automatically verify} bisimulation--like
	   relations between processes by means of {\em model checking}.

	   (revised February 1992)