A Branching Time Logical System for Open Distributed Systems Development

We propose a new first-order many-sorted branching-time logical system with equality devoted to support the development of open distributed systems. The inherent characteristics of this family of systems, which ought to be treated in rigorous software development processes, are used throughout the paper to motivate the specific features of our formalism. We present a solution of the drinking philosophers problem as a way of illustrating the application of this new logical system.