A FRAGMENT OF 1ST-ORDER LOGIC ADEQUATE FOR OBSERVATION EQUIVALENCE


OGUZTUZUN H.

LECTURE NOTES IN COMPUTER SCIENCE, cilt.626, ss.278-292, 1992 (SCI İndekslerine Giren Dergi) identifier

  • Yayın Türü: Makale / Tam Makale
  • Cilt numarası: 626
  • Basım Tarihi: 1992
  • Dergi Adı: LECTURE NOTES IN COMPUTER SCIENCE
  • Sayfa Sayıları: ss.278-292

Özet

We present a logical characterization of the Milner's notion of observation equivalence of processes (''at most one observable action at a time'' variant) by using a restricted class of first order formulas. We use the game technique due to Ehrenfeucht as a means to achieve this characterization. First we extend the Ehrenfeucht game by introducing a pair of compatibility relations as a parameter to the game so that we can restrict the moves of the players on the basis of the previous moves. We then define the logic which corresponds to the extended game. Second we characterize the observation equivalence on a restricted class of labelled transition systems (with tau moves), called trace-unique labelled transition systems (t-taults's), as the equivalence induced by the games played on certain reducts of the given t-taults's where the compatibility relations are defined in terms of bounded reachability in the t-taults's. Combining these two characterizations we get our main result.