L&CThe Logic and Computation Group

This group uses logic and related techniques to model, specify, verify and reason about computational processes, and in particular, those of complex, reactive and dynamic systems. Automated reasoning algorithms and tools are developed to be used to verify the correctness, reliability or security of such systems.

Projects and Research Grants

ARC Discovery Project2011-2013255,000Automation of metric temporal reasoning
The UWA Research Grants Scheme2008-200910,000A formal framework for the refinement and abstraction of security protocols
French-Australian Science and Technology200810,000 Formal framework for the refinement of secure communication protocols
ARC Discovery2004-2008500,000 Combining modal logics for dynamic and multi-agent systems (with Sattar et al)
Large ARC
2000-2002~176,000Proof theory for combinations of temporal and epistemic logic (with R. van der Meyden)
Small ARC199912,000 Reasoning about complex systems
Small Internal Grants
Small Internal grants for projects relating to Parallel Computing, Automated Reasoning, Artificial Intelligence, a Logic of Robustness and Bioinformatics



  1. Prof. Mark Reynolds (Head of Logic and Computation Group)
  2. A/Prof. Tim French
  3. Dr Rowan Davies
  4. Dr John McCabe-Dansted


Significant Publications

[1] Mark Reynolds. A tableau for CTL*. In Ana Cavalcanti and Dennis Dams, editors, FM, volume 5850 of Lecture Notes in Computer Science, pages 403-418. Springer, 2009. [ bib ]
[2] D.M. Gabbay, I. Hodkinson, M.A. Reynolds, and M. Finger. Temporal logic: mathematical foundations and computational aspects. Oxford University Press, USA, 2000. [ bib ]
[3] Mark Reynolds. An axiomatization of full computation tree logic. J. Symb. Log., 66(3):1011-1057, 2001. [ bib ]
[4] Mark Reynolds. The complexity of the temporal logic with "until" over general linear time. J. Comput. Syst. Sci., 66(2):393-426, 2003. [ bib ]
[5] T.N. French. Bisimulation quantifiers for modal logics. 2006. [ bib ]
[6] Tim French, John Christopher McCabe-Dansted, and Mark Reynolds. A temporal logic of robustness. In Boris Konev and Frank Wolter, editors, FroCos, volume 4720 of Lecture Notes in Computer Science, pages 193-205. Springer, 2007. [ bib ]