Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Eleventh Annual IEEE Symposium on

Logic in Computer Science (LICS 1996)

Paper: Locally linear time temporal logic (at LICS 1996)

Authors: Ramaswamys Ramanujam

Abstract

We study linear time temporal logics of multiple agents, where the temporal modalities are local. These modalities not only refer to local next-instants and local eventuality, but also global views of agents at any local instant, which are updated due to communication from other agents. Thus agents also reason about the future, present and past of other agents in the system. The models for these logics are simple : runs of networks of synchronizing automata. Problems like gossipping in interconnection networks are naturally described in the logics proposed here. We present solutions to the satisfiability and model checking problems for these logics. Further, since formulas are insensitive to different interleavings of runs, partial order based verification methods become applicable for properties described in these logics.

BibTeX

  @InProceedings{Ramanujam-Locallylineartimete,
    author = 	 {Ramaswamys Ramanujam},
    title = 	 {Locally linear time temporal logic},
    booktitle =  {Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS 1996)},
    year =	 {1996},
    month =	 {July}, 
    pages =      {118--127},
    location =   {New Brunswick, NJ, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2017-04-0512:37
Andrzej Murawski