Tense logics for local reasoning in distributed systems
We treat the notion of agent as primary in the definition of concurrency. Our computation models, ACSAs and CSAs, come from [LRT], which axiomatizes these two classes along with various subclasses. The language considered in [LRT, LT] can be obtained by closing propositions from P ∪ T under boolean operations and the agent-indexed modalities ⊟i and □i, i ε ℕ.
R. Parikh pointed out [Pa] that the logic in [LT] could be translated into basic tense logic with agent propositions. The language Ψ is much simpler while still retaining the “local future” abilities: we have eliminated the agent propositions and demonstrated that our systems can be axiomatized either by using agent propositions or by using indexed modalities as preferred. As a technical improvement, we note that the axiomatizations of ACSAs and CSAs in [LRT] used an inference rule (TE) to enforce an event to be within an agent, which is shown to be unnecessary.
The main technical question which remains is that of decidability. The logic Φ is easily seen to be decidable by way of the decidability of Tense S4. We conjecture that all the other logics we have considered are decidable.
Unable to display preview. Download preview PDF.
- [B]J. P. Burgess, “Basic tense logic”, in Handbook of Philosophical Logic, Vol. II, eds. D. Gabbay and F. Guenthner (D. Reidel Publishing Company, Dordrecht, 1984) 89–133.Google Scholar
- [HM]J. Y. Halpern and Y. Moses, “Knowledge and common knowledge in a distributed environment”, Proc. 3rd ACM PODC (1984) 50–61.Google Scholar
- [LR]K. Lodaya and R. Ramanujam, “Tense logics for local reasoning in distributed systems”, IMSc Report (1991).Google Scholar
- [LRT]K. Lodaya, R. Ramanujam and P. S. Thiagarajan, “Temporal logics for communicating sequential agents I”, IMSc Report 89/12 (1989).Google Scholar
- [LT]K. Lodaya and P. S. Thiagarajan, “A modal logic for a subclass of event structures”, LNCS 267 (1987) 290–303.Google Scholar
- [LTa]K. Lodaya and P. S. Thiagarajan, “A correction to ‘A modal logic for a subclass of event structures'”, Report DAIMI-PB-275, Computer Science Department, Aarhus University, (Aarhus, 1989).Google Scholar
- [NPW]M. Nielsen, G. Plotkin and G. Winskel, “Petri nets, event structures and domains I”, TCS 13, 1 (1980) 86–108.Google Scholar
- [Pa]R. Parikh, personal communication (1987).Google Scholar