A spatial logic for concurrency. I (Q1887152)

A logic which can express properties of freshness, secrecy, structure and behavior of concurrent systems is presented. It contains spatial operations corresponding to composition, local name restriction and primitive fresh name quantifier. At the beginning short review of the asynchronous \(\pi\)-calculus is given. Later a detailed presentation of the syntax of the spatial logic, its semantics, and logical validity are studied. At the end, fresh and hidden name quantifications and the recursive definition properties are motivated and discussed.