EPSRC Grant: GR/S49353/01

2006

1. (co-author A. Lomuscio and F.Raimondi) Verification of the TESLA protocol in MCMAS-X. In Proceedings of the International Workshop on Concurrency, Specification and Programming (CS&P'06), pp. 255 - 267. Wandlitz (nearby Berlin), Germany, 27-29 September 2006.
   Display in BibTex Format
2. (co-author A. Lomuscio and A. Zbrzezny) Bounded Model Checking real-time multi-agent systems with clock differences: theory and implementation. In Proceedings of the 4th International Workshop on Model Checking and Artificial Intelligence (MoChArt'06). August, 2006.
   Also, Technical report RN/06/03, Department of Computer Science, University College London. March, 2006. (pdf).
   Display in BibTex Format
3. (co-author A. Lomuscio) A complete and decidable axiomatisation for deontic interpreted systems. In Proceedings of the 8th International Workshop on Deontic Logic in Computer Science (DEON'06). LNCS, volume 4048, pp. 238 - 254. Springer Berlin / Heidelberg. Utrecht, The Netherlands. July 2006.
   Also, Technical report RN/06/17, Department of Computer Science, University College London. June, 2006. (pdf). Display in BibTex Format
4. (co-author A. Lomuscio) A complete and decidable security-specialised logic and its application to the TESLA protocol. In Proceedings of the 5th International Joint Conference on Autonomus Agents and Multi Agent Systems (AAMAS'06). ACM Press, pp. 145-152. Hakodate, Japan, 2006.
   Display in BibTex Format

2005

1. (co-author A. Lomuscio) A Temporal Epistemic Logic with a Reset Operation. Technical report RN/05/27, Department of Computer Science, University College London. November 2005. (pdf).
2. (co-author A. Lomuscio) A combination of explicit and deductive knowledge with branching time: completeness and decidability results. In the post-proceedings of the International Workshop on Declarative Agent Languages and Technologies (DALT'05). LNCS, volume 3904, pp. 188-204. Springer Berlin / Heidelberg, 2006. Also, in proceedings of the International Workshop on Concurrency, Specification and Programming (CS&P'05). Ruciane Nida, Poland. September 2005. Also, Technical Report RN/05/18, Department of Computer Science, University College London. August, 2005. (pdf).
   Display in BibTex Format
3. (co-author A. Lomuscio and W.Penczek) Bounded Model Checking for Knowledge and Real Time. In Proceedings of the 4th International Joint Conference on Autonomus Agents and Multi Agent Systems (AAMAS'05). ACM Press, pp. 165-172. 2005.
   Display in BibTex Format
4. (co-author A. Lomuscio) A Logic for Knowledge, Correctness, and Real Time. In Proceedings of the 5th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA'04). LNAI, volume 3487. Springer-Verlag, pp. 1-15. 2005.
   Display in BibTex Format

2004

1. Bożena Woźna and A. Zbrzezny. Checking ACTL* properties of Discrete Timed Automata via Bounded Model Checking. (Revised version of the paper published in Proceedings of the 1st International Workshop on Formal Analysis and Modeling of Timed Systems (FORMATS'03)). Technical Report TR-04-04, Department of Computer Science, King's College London, 2004.
   Display in BibTex Format
2. ACTL* properties and Bounded Model Checking. Fundamenta Informaticae 63(1) pp. 65-87, 2004.
   Display in BibTex Format
3. (co-author A. Lomuscio and W. Penczek) Bounded Model Checking for Deontic Interpreted Systems. Electronic Lecture Notes in Theoretical Computer Science, volume 126, pp. 93-114, 2004. (A previous version of this paper appeared in the proceedings of LCMAS04. Second Workshop on Logic and Communication in Multi-Agent Systems. Nancy, August, 2004.)
   Display in BibTex Format
4. (co-authors A. Lomuscio and W. Penczek) Bounded model checking for knowledge over real time. In Proceedings of Concurrency Specification and Programming (CS&P'04). Potsdam, September, 2004.
   Display in BibTex Format
5. (co-authors W. Penczek, A. Półrola, and A. Zbrzezny) Bounded Model Checking for Reachability Testing in Time Petri Nets. In Proceedings of Concurrency Specification and Programming (CS&P'04). Potsdam, September, 2004.
   Display in BibTex Format