Computer Science – Logic in Computer Science
Scientific paper
2011-09-20
Computer Science
Logic in Computer Science
54 pages, submitted. Expanded version of ICE '11 paper
Scientific paper
10.4204/EPTCS.59.2
Seeking a general framework for reasoning about and comparing programming languages, we derive a new view of Milner's CCS. We construct a category E of 'plays', and a subcategory V of 'views'. We argue that presheaves on V adequately represent 'innocent' strategies, in the sense of game semantics. We equip innocent strategies with a simple notion of interaction. We then prove decomposition results for innocent strategies, and, restricting to presheaves of finite ordinals, prove that innocent strategies are a final coalgebra for a polynomial functor derived from the game. This leads to a translation of CCS with recursive equations. Finally, we propose a notion of 'interactive equivalence' for innocent strategies, which is close in spirit to Beffara's interpretation of testing equivalences in concurrency theory. In this framework, we consider analogues of fair testing and must testing. We show that must testing is strictly finer in our model than in CCS, since it avoids what we call 'spatial unfairness'. Still, it differs from fair testing, and we show that it coincides with a relaxed form of fair testing.
Hirschowitz Tom
Pous Damien
No associations
LandOfFree
Strategies as sheaves and interactive equivalences for CCS does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Strategies as sheaves and interactive equivalences for CCS, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Strategies as sheaves and interactive equivalences for CCS will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-147740