4
$\begingroup$

Vijay D alluded to the relation between the fundamental theorem of Ehrenfeucht-Fraisse games and notions of bisimulation and simulation in response to the whats-a-magical-theorem-in-logic question.

The notion of simulation was defined as weak homomorphism between two program milner71. While Fraisse theorem provides an algebraic characterization of elementary equivalence between two (FOL) structures. Further elementary equivalence between two structures imply that the structures preserves all (FOL definable) properties. So the connection is difficult to miss.

Are there reference to books/papers that make this connection explicit and study it systematically. By "systematic", I am looking at gradual "weakening" of the relation between two structures (starting from isomorphism) and the corresponding set of logical formulas say mu-calculus that are preserved. A connection to program verification (and in particular concurrency) would be desirable in these references.

Improve this question
$\endgroup$
2
  • $\begingroup$ Bisimulation equivalence is the same as e.g. CTL or CTL* equivalence; is this the kind of connection you are looking for? $\endgroup$
    – Sylvain
    Commented Mar 18, 2014 at 20:03
  • $\begingroup$ Yes that is an instance of the connection between algebraic notions of equivalence in process algebra and the temporal logical equivalence. Adequacy of logic [HM] with respect to a given equivalence relation on language of processes is one notion that has been use to relate the notions back to logic. I am hoping for reference where these notions of equivalence are systematically studied as relation between two structures with respect to the first order logic. These structures can then be "later" thought of as finite state automata or transition systems. $\endgroup$
    – Mitesh J
    Commented Mar 18, 2014 at 22:54

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .