Publications 2004

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.

Year 2004

• 1) 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 (LCMAS04), Nancy, July, 2004 PDF.gz file - WoznaLomuscioPenczek-lcmas04.pdf.gz

• 2) 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

• 3) 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

• 4) 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

• 5) 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

• 6) 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

• 7) 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

• 8) 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

• 9) 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

• 10) 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

• 11) 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

• 12) 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

• 13) 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

• 14) 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

• 15) 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