Publications 2006, 2005, 2004, 2003, 2002, 2000 - 2001, 1992 - 1999

Most of the papers available from this document appear in print, and the corresponding copyright is held by the publisher. While the papers can be used for personal use, redistribution or reprinting for commercial purposes is prohibited.

in the reverse chronological order

Year 2006

M. Kacprzak, A. Lomuscio, A. Niewiadomski, M. Szreter, W. Penczek, F. Raimondi, Comparing BDD and SAT based techniques for model checking Chaum's Dining Cryptographers Protocol, to appear Fundamenta Informaticae, 2006. PS.gz file - klnspr-fi06.ps.gz

B. Konikowska, W. Penczek, Model Checking for Multivalued Logic of Knowledge and Time, Proc. of AAMAS'06, ACM, 2006. PDF.gz file - kp-AAMAS06.pdf.gz

Year 2005

B. Wozna, A. Lomuscio, W. Penczek, Bounded model checking for deontic interpreted systems, Proceedings of the second Workshop on Logic and Communication in Multi-Agent Systems, wersja finalna, ENTCS: 93-114, 2005.

B. Wozna, A. Lomuscio, W. Penczek, Bounded model checking for Knowledge and real Time, Proc. of AAMAS'05, ACM, 2005.

M. Kacprzak and W. Penczek, Fully Symbolic Unbounded Model Checking for Alternating-Time Temporal Logic, Autonomous Agents and Multi-Agent Systemc (Springer Science + Business Media), 11, 69-89, 2005.

A. Niewiadomski, W. Penczek, M. Szreter, M. Kacprzak, Model Checking Dining Cryptographers with Verics, Proc. of CSP'05, 2005. PS.gz file - npsk-csp05.ps.gz

G. Jakubowska, W. Penczek, M. Srebrny, Verifying Security Protocols with Timestamps via Translation to Timed Automata, Proc. of CSP'05. 2005. PS.gz file - jps-csp05.ps.gz

A. Lomuscio, W. Penczek, "Verification of multi-agent systems via model checking", Proc. of Summer School EASSS'05, 2005. PS.gz file - lp-easss05.ps.gz

Year 2004

M. Kacprzak, A. Lomuscio, W. Penczek, From bounded to Unbounded model checking for temporal epistemic logic, to appear in Fundamenta Informaticae, 2004, PS.gz file - BvU-FI.ps.gz

B. Wozna, A. Lomuscio, W. Penczek, Bounded model checking for knowledge over real time, Proc. of CSP'04, 2004, PS.gz file - WLP-CSP04.ps.gz

M. Kacprzak, A. Lomuscio, W. Penczek, Verification of multiagent systems via unbounded model checking, Proc. of AAMAS'04, pp. 638 - 645, 2004, Editors: N. R. Jennings, C. Sierra, L. Sonenberg and M. Tambe, PS.gz file - Kacprzak-Lomuscio-Penczek-UMC-updated.ps.gz

M. Kacprzak and W. Penczek, Unbounded Model Checking for Alternating-Time Temporal Logic, Proc. of AAMAS'04, pp. 646 - 653, 2004, Editors: N. R. Jennings, C. Sierra, L. Sonenberg and M. Tambe, PS.gz file - Kacprzak-Penczek-UMC-ATL.ps.gz

M. Kacprzak and W. Penczek, Model Checking for Alternating-Time mi-Calculus via Translation to SAT, Proc. of CSP'04, 2004, PS.gz file - AMC-CSP04.ps.gz

M. Kacprzak and W. Penczek, A SAT-based Approach to Unbounded Model Checking for Alternating-Time Temporal Epistemic Logic, to appear in Knowledge, Rationality and Action, Kluwer, 2004, PS.gz file - ATLEL-KRA.ps.gz

W. Penczek and A. Polrola, Specification and Model Checking of Temporal Properties in Time Petri Nets and Timed Automata, Proc. of ICATPN'04, 2004, PS.gz file - ATPN04-LNCS.ps.gz

W. Penczek, A. Polrola, B. Wozna, A. Zbrzezny, Bounded Model Checking for Reachability Testing in Time Petri Nets, Proc. of CSP'04, 2004, PS.gz file - bmctpn-csp04-final.pdf.gz

B. Konikowska and W. Penczek, On designated values in multi-valued CTL* model checking, Fundamenta Informaticae, pp. 211 - 224, 2004, PS.gz file - konikowska-penczek-fi04.ps.gz

B. Konikowska and W. Penczek, Model Checking Multi-Valued Modal Mi-Calculus: Revisited, Proc. of CS&P'04, 2004, PS.gz file - KP-CSP04.ps.gz

A. Polrola and W. Penczek, Minimization Algorithms for Time Petri Nets, Fundamenta Informaticae, Vol. 60(1-4), pp. 307 - 331, 2004, PS.gz file - polrola-penczek-fi04.ps.gz

W. Nabialek, A. Niewiadomski, W. Penczek, A. Polrola, M. Szreter, VERICS 2004: A Model Checker for Real Time and Multi-agent Systems, Proc. of CSP'04, 2004 PS.gz file - verics2004-final-CSP04.pdf.gz

M. Kacprzak, A. Lomuscio, T. Lasica, W. Penczek, M. Szreter, Verifying Multi-agent Systems via Unbounded Model Checking results, To appear in Proceedings of the Third NASA Workshop on Formal Approaches to Agent-Based Systems FAABS III. To appear in LNAI 3228, pp. 189 - 212, 2005 PS.gz file - FAABS2004.pdf.gz

A. Polrola, W. Penczek, M. Szreter, Towards Efficient Partitioning Refinement for Checking Reachability in Timed Automata, Proc. of FORMATS'03, LNCS 2791, pp. 2 - 17, 2004, PS.gz file - FORMATS03.ps.gz

Year 2003

(co-author M. Kacprzak and A. Lomuscio) Unbounded model checking for knowledge and time, Report 966, 2003, PS file - report966-UMC03.ps

(co-author A. Polrola) Minimization algorithms for Time Petri Nets, Proc. of CS&P'03, 2003, PS.gz file - csp03-pp.ps.gz

(co-author B. Konikowska) On designated values in multi-valued CTL* model checking, Proc. of CS&P'03, 2003, PS.gz file - kp-csp03.ps.gz

(co-author M. Kacprzak and A. Lomuscio) Unbounded model checking for knowledge and time, Proc. of CS&P'03, 2003, PS.gz file - klp-csp03.ps.gz

(co-author P. Dembinski, A. Janowska, P. Janowski, A. Polrola, M. Szreter, B. Wozna, A. Zbrzezny) VERICS: Weryfikator dla automatow czasowych i specyfikacji zapisanych w jezyku ESTELLE, Proc. of SCR'03, PS.gz file - scr03.ps.gz

(co-author A. Polrola, M. Szreter) Reachability Analysis for Timed Automata based on Partitioning, ICS PAS Report 961, 2003, PS.gz file - tr961.ps.gz

(co-author P. Dembinski, A. Janowska, P. Janowski, A. Polrola, M. Szreter, B. Wozna, A. Zbrzezny) VERICS: A Tool for Verifying Timed Automata and Estelle Specifications, Proc. of TACAS'03, LNCS 2619, pp. 278 -- 283, 2003. PS.gz file - verics.ps.gz

(co-author A. Lomuscio, T. Lasica) Bounded Model Checking for interpreted systems: preliminary experimental results, Proc. of FAABS II, LNCS 2699, 2003. PS.gz file - faabs2003.ps.gz

(co-author A. Lomuscio) Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking, Proc. of AAMAS'03, in T. Sandholm, editor, 2003. PS.gz file - aamas2003.ps.gz

(co-author M. Kacprzak, A. Lomuscio) Bounded versus Unbounded Model Checking for Interpreted Systems, invited talk at FAAMAS'03, pp. 5 - 20, B. Dunin-Keplicz, R. Verbrugge, editors, 2003. PS.gz file - famas2003.ps.gz

(co-author A. Polrola, M. Szreter) Reachability Analysis for Timed Automata Using Partitioning Algorithms, Fundamenta Informaticae, Vol. 55(2), pp. 203-221, 2003, PS.gz file - fi-pps03.ps.gz

(co-author A. Lomuscio) Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking, Fundamenta Informaticae, Vol. 55(2), pp. 167-185, 2003, PS.gz file - fi-pl03.ps.gz

(co-author B. Wozna, A. Zbrzezny) Checking Reachability Properties for Timed Automata via SAT, Fundamenta Informaticae, Vol. 55(2), pp. 223-241, 2003, PS.gz file - fi-pps03.ps.gz

Year 2002

(co-author B. Wozna and A. Zbrzezny) Bounded Model Checking for the Universal fragment of CTL, Fundamenta Informaticae, 2002. PS.gz file - fi02-abw.ps.gz

(co-author B. Konikowska) Model Checking for Multi-Valued CTL*, a chapter in the book on Multi-Valued Logics, M. Fitting and E. Orlowska eds., 2002. PS.gz file - MVL-bookchapter.ps.gz

(co-author P. Dembinski and A. Polrola) Verification of Timed Automata Based on Similarity, Fundamenta Informaticae, 2002. PS.gz file - fi02-dpp.ps.gz

(co-author B. Wozna and A. Zbrzezny) Bounded Model Checking for Elementary Nets Systems, ICS PAS Report 940, 2002. PS.gz file - raport940-abw02.ps.gz

(co-author B. Konikowska) Reducing Model Checking from Multi-Valued CTL* to CTL*, Proc. of CONCUR'02, LNCS 2421, 2002. PS.gz file - concur02.ps.gz

(co-author B. Wozna and A. Zbrzezny) Towards Bounded Model Checking for the Universal Fragment of TCTL, Proc. of FTRTFT'02, LNCS 2469, 2002. PS.gz file - ftrtft02.ps.gz

(co-author H. Hansen and A. Valmari) Stuttering-Insensitive Automata for On-the-fly Detection of Livelock Properties, Proc. of FMICS'02, 2002. PS.gz file - fmics02.ps.gz

(co-author A. Lomuscio) Bounded Model Checking for Interpreted Systems, ICS PAS Report 946, 2002. PS.gz file - TR946.ps.gz

(co-author B. Wozna and A. Zbrzezny) Towards Bounded Model Checking for the Universal Fragment of TCTL, ICS PAS Report 947, 2002. PS.gz file - TR947.ps.gz

(co-author B. Wozna and A. Zbrzezny) Checking Reachability Properties via SAT, ICS PAS Report 949, 2002. PS.gz file - report949.ps.gz

Years 2000 - 2001

(co-author S. Ambroszkiewicz and T. Nowak) Towards Formal Specification and Verification in Cyberspace. In Proc. The first Goddard Workshop on Formal Approaches to Agent-Based Systems, LNAI 1871, pp. 16 - 32, 2001. PS.gz file - goddard00.ps.gz

(co-author S. Ambroszkiewicz and K. Cetnarowicz) Modeling Agent Organizations. In Proc. Advances in soft computing, Bystra, Poland, June 12-16, 2000

Temporal Approach to Causal Knowledge, International Journal of the IGPL, Vol. 8(1), pp. 87--99, 2000. PS.gz file - igpl00.ps.gz

(co-author M. Szreter, R. Gerth, and R. Kuiper)) Improving Partial Order Reductions for Universal Branching Time Properties, Fundamenta Informaticae 43, 2000. PS.gz file - FI00.ps.gz

(co-author M. Szreter) More than one, less than all: Linear to Branching revisited, Proc. of CS\&P, Berlin, 2000.

(co-author M. Szreter) Automatyczna weryfikacja systemow czasu rzeczywistego, Proc. of SCR, Krak/ow, 2000. PS.gz file - scr00.ps.gz

"Abstractions and partial order reductions for checking branching properties of Time Petri Nets", Proc. of ICATPN, LNCS 2075, pp. 323--342, 2001. PS.gz file - icatpn01.ps.gz

Model checking for modal logics, Proc. of Workshop on Theory and Applications of Multiple-Valued Logic, pp. 85 -- 90, 2001. PS.gz file - mvl01.ps.gz

A local approach to modal logic for multi-agent systems, Proc. of Workshop on Logic and Logical Philosophy, Dresden, 2001. PS.gz file - llp01.ps.gz

Efficient model checking of causal-knowledge protocols, Proc. of CEEMAS'01, pp. 217 -- 226, 2001 to appear in LNCS. PS.gz file - ceemas01.ps.gz

(co-author P. Dembinski and A. Polrola) Automated verification of infinite state concurrent systems: an improvement in model generation, Proc. of PPAM'01, to appear in LNCS, 2001. PS.gz file - ppam01.ps.gz

Years 1992 - 1999

(co-author R. Kuiper and U. Goltz) Propositional temporal logics and equivalences, Proc. of International Conference on Concurrency Theory, LNCS 630, pp. 222-236, 1992. PS.gz file - concur92.ps.gz

On temporal logics for trace systems, Proc. of ASMICS Workshop, Bericht 4-92, Universitat Stuttgart, pp. 158-204, 1992.

On undecidability of propositional temporal logics on trace systems, Information Processing Letters 43, pp. 147-153, 1992. PS.gz file - ipl92.ps.gz

Temporal Logics for Trace Systems: On automated verification, International Journal of Foundations of Computer Science, Vol. 4 No. 1, pp. 31-67, 1993. PS.gz file - ijfcs93.ps.gz

Axiomatizations of Temporal Logics on Trace Systems, Proc. of Symposium on Theoretical Aspects of Computer Science, LNCS 665, pp. 452 - 462, 1993. PS.gz file - stacs93.ps.gz

(co-author R. Kuiper) Verification by hand using linear time temporal logic, a book chapter of "Logic: Mathematics, Language, Computer science and Philosophy", Vol. II, Edit. H.S. de Swart, Publ. Peter Lang GMbh, pp. 229--252, 1994.

(co-author R. Kuiper) Automated verification using branching time temporal logic, a book chapter of "Logic: Mathematics, Language, Computer science and Philosophy", Vol. II, Edit. H.S. de Swart, Publ. Peter Lang GMbh, pp. 252--262, 1994.

(co-author M. Kwiatkowska i D. Peled) A Hierarchy of Partial Order Temporal Properties, Proceedings of the 1st International Conference on Temporal Logic, Bonn, Germany, Springer-Verlag, LNAI 827, pp. 398--414, 1994. PS.gz file - ictl94.ps.gz

(co-author R. Gerth, R. Kuiper, and D. Peled) A Partial Order Approach to Branching Time Logic Model Checking, Proceedings of the Israeli Conference on Theoretical Computer Science, IEEE Computer Society Press, pp. 130-139, 1995. PS.gz file - istcs95.ps.gz

(co-author P. Niebert) On the connection of partial order logics and partial order reductions, Raport TUE 95-15, Eindhoven University, 1995. PS.gz file - TUE95-15.ps.gz

Branching time and partial order in temporal logics, a book chapter of "Time and Logic: A Computational Approach". (L. Bolc, A. Szalas, eds.), UCL Press Ltd. London 1995. PS.gz file - chapter95.ps.gz

(co-author Kuiper, R.): "Traces and Logic", TUE Computing Science Report 94-52, a book chapter of "The Book of Traces", ed. V. Diekert, G. Rozenberg, World Scientific Publishing in Singapore, 1995. PS.gz file - habilitation95.ps.gz

(co-author R. Alur i D. Peled) Model-Checking of Causality Properties, Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, San Diego, USA, pp. 100--110, 1995. PS.gz file - lics95.ps.gz

(co-author D. Peled) Using Asynchronous Buchi Automata for Efficient Automatic Verification of Concurrent Systems, Proceedings of the 15th IFIP WG 6.1 Symposium on Protocol Specification, Testing and Verification, Warsaw, eds. P. Dembinski, M. /Sredniawa, pp. 115--130, Chapman & Hall, 1996 PS.gz file - pstv96.ps.gz

Proceedings of MFCS'96 (editor), LNCS 1113, pp. 592, 1996.

Axiomatizations of Temporal Logics on Trace Systems, Fundamenta Informaticae 25, pp. 183--200, 1996. PS.gz file - FI96.ps.gz

(co-author Srebrny, M.) First-order temporal logic over trace systems, Proceedings of POMIV'96, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Volume 29, pp. 79--97, 1997. PS.gz file - POMIV96.ps.gz

Model checking for a Fragment of Event Structures, Proceedings of TACAS'97, LNCS 1217, pp. 146--164, 1997. PS.gz file - tacas97.ps.gz

Special Isuue of TCS 195 (editor), pp. 80, 1998.

(co-authors R. Gerth i R. Kuiper) Partial Order Reductions Preserving Simulations, IPI PAN Raport 843, 1997. PS.gz file - IPI843-97.ps.gz

(co-author S. Ambroszkiewicz) Modeling rational BDI-agents within the framework of asynchronous automata, Proc. of CS&P'97, pp. 1--19, IPI PAN Report 832, 1997. PS.gz file - CSP97.ps.gz

(co-author S. Ambroszkiewicz, O. Matyja) Team formation in a distributed environment: the idea and algorithms, < IPI PAN, Report 855, 1998. PS.gz file - IPI855.ps.gz

Temporal logic of causal knowledge, Proc. of WoLLIC'98, pp. 178 - 187, Sau Paulo, 1998. PS.gz file - wollic98.ps.gz

(co-author S. Ambroszkiewicz, O. Matyja) Team Formation by Self-Interested Mobile Agents. In Chengqi Zhang and Dickson Lukose (Eds.) Multi-Agent Systems, Proc. of 4th Australian DAI Workshop, Brisbane, 1998, LNAI 1544. PS.gz file - DAI98.ps.gz

(co-author S. Ambroszkiewicz, O. Matyja) Cooperation Mechanisms in a Multi-Agent Distributed Environment. In Proc. ECAI-98 Workshop 8: Synthesis of Intelligent Agent Systems from Experimental Data, (J. Komorowski, A. Skowron, and I. Duntsch Eds.), Brighton, UK, 1998. PS.gz file - ecai98.ps.gz

Proceedings of the Multi-Agent Day, (editor), Warsaw, A one day workshop held at IPI PAN, ISBN 83-910948-0-4, 1998.

(co-author S. Ambroszkiewicz) Distributed games: local interactions, explicit communication, and causal knowledge, IPI PAN Report 873, 1999. Proc. of Third Conference on Logic and the Foundations of Game and Decision Theory (LOFT3), Turyn, 1998. PS.gz file - LOFT98.ps.gz

(co-author S. Ambroszkiewicz) Model checking of local knowledge formulas, Proc. of FCT'99 Workshop on Distributed Systems, Vol. 28 in Electronic Notes in Theoretical Computer Science, 1999. PS.gz file - entcs99.ps.gz

(co-author S. Ambroszkiewicz) Local interactions, explicit communication, and causal Knowledge in Games and Multi-Agent Systems. Proc. of CEEMAS'99, St. Petersburg, 1999. PS.gz file - penczek99.ps.gz

(co-authors R. Gerth, R. Kuiper, M. Szreter) Partial Order Reductions Preserving Simulations, Proc. of CS&P'99, Warsaw, PS.gz file - CSP99.ps.gz

(co-authors R. Gerth, R. Kuiper i D. Peled) A partial order approach to branching time logic model-checking, Information and Computation, 1999. PS.gz file - IC99.ps.gz