Coordination Logic
Bernd Finkbeiner and Sven Schewe
We introduce Coordination Logic (CL), a new temporal logic that reasons about the interplay between behavior and informedness in distributed systems. CL provides a logical representation for the distributed realizability problem and extends the game-based temporal logics, including the alternating-time temporal logics, strategy logic, and game logic, with quantification over strategies under incomplete information. We show that the structure in CL that results from the nesting of the quantifiers is sufficient to guarantee the decidability of the logic and at the same time general enough to subsume and extend all previously known decidable cases of the distributed realizability problem.
19th EACSL Annual Conference on Computer Science Logic (CSL 2010).