Bisimulations and predicate logic.

*(English)*Zbl 0809.03018First, some basic results concerning the coinductive characterization of bisimilarity are presented. It is proved that bisimilarity is not preserved under elementary substructures and it is analyzed how certain transitions defined from data models depend on data by turning a bisimulation into an isomorphism between the data models. The data dependence of transitions is shown to be first-order by internalizing nondeterminism in states given as sets. Further, bisimulation is studied as an extensional notion of equivalence on programs, generalizing input/output equivalence (a \(\Pi^ 0_ 2\)-notion), an equivalence that may fall outside of \(\Pi^ 1_ 1\). This explosion in logical complexity is a measure of the scope of bisimilarity resting heavily on infinite branching.

Reviewer: D.Gruska (Bratislava)

##### Keywords:

semantics; transition system; modal logic; first-order logic; coinductive characterization of bisimilarity; bisimulation; nondeterminism; equivalence on programs; logical complexity; infinite branching
Full Text:
DOI

##### References:

[1] | Every recursive linear ordering has a copy in DTIME-SPACE(n. log(n)) 55 pp 571–575– (1990) |

[2] | Handbook of philosophical logic 2 (1984) |

[3] | Proceedings of the American Mathematical Society 54 pp 311–315– (1976) |

[4] | Modal logic and classical logic (1985) · Zbl 0639.03014 |

[5] | Logic of transition systems (1993) |

[6] | Admissible sets and structures (1975) |

[7] | The next admissible set 36 pp 108–120– (1971) |

[8] | Process algebra 18 (1990) · Zbl 0716.68002 |

[9] | Non-well-founded sets (1988) |

[10] | Handbook of Mathematical Logic (1977) |

[11] | Proceedings, seventh annual symposium on logic in computer science (1992) |

[12] | Proceedings of the REX Workshop 666 (1993) |

[13] | Information and Computation 92 pp 161–218– (1991) |

[14] | Handbook of logic in computer science 2 (1992) |

[15] | A structural approach to operational semantics (1981) |

[16] | A path from generalized recursion back to mechanical computation (1993) |

[17] | Computer science logic: Selected papers from CSL ’92 702 (1993) |

[18] | Logics in AI 633 (1992) |

[19] | Incompleteness along paths in progressions of theories 27 (1962) |

[20] | Semantics of systems of concurrentprocesses 469 (1990) |

[21] | Information and computation 99 (1992) |

[22] | Proceedings, eighth annual symposium on logic in computer science (1993) |

[23] | Journal of the Association for Computing Machinery (1988) |

[24] | Which program constructions are safe for bisimulation? (1993) |

[25] | Language in action: Categories, lambdas and dynamic logic (1991) · Zbl 0717.03001 |

[26] | Proceedings of the 5th GI Conference 104 pp 167–183– (1981) |

[27] | Communication and concurrency (1989) · Zbl 0683.68008 |

[28] | Handbook of mathematical logic (1977) |

[29] | Studies in model theory (1973) |

[30] | Journal of the Association for Computing Machinery 32 (1985) |

[31] | Bulletin of the Polish Academy of Science 8 (1960) |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.