Show/Hide Menu
Hide/Show Apps
anonymousUser
Logout
Türkçe
Türkçe
Search
Search
Login
Login
OpenMETU
OpenMETU
About
About
Açık Bilim Politikası
Açık Bilim Politikası
Frequently Asked Questions
Frequently Asked Questions
Browse
Browse
By Issue Date
By Issue Date
Authors
Authors
Titles
Titles
Subjects
Subjects
Communities & Collections
Communities & Collections
A fragment of first order logic adequate for observation equivalence
Date
1992-01-01
Author
Oğuztüzün, Mehmet Halit S.
Metadata
Show full item record
This work is licensed under a
Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License
.
Item Usage Stats
3
views
0
downloads
© Springer-Verlag Berlin Heidelberg 1992.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 τ moves), called trace-unique labelled transition systems (τ-lts’s), as the equivalence induced by the games played on certain rcducts of the given τ-lts’s where the compatibility relations are defined in terms of bounded reachability in the τ-lts’s. Combining these two characterizations we get our main result.
Subject Keywords
Order Logic
,
Atomic Formula
,
Predicate Symbol
,
Winning Strategy
,
Label Transition System
URI
https://hdl.handle.net/11511/57706
DOI
https://doi.org/10.1007/bfb0023774
Collections
Department of Computer Engineering, Conference / Seminar