Selected Publications 2019 - 1992

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.

2019

• Artur Niewiadomski, Piotr Switalski, Teofil Sidoruk, Wojciech Penczek: Applying Modern SAT-solvers to Solving Hard Problems. Fundam. Inform. 165(3-4): 321-344 (2019)

• Wojciech Penczek: All True Concurrency Models Start with Petri Nets: A Personal Tribute to Carl Adam Petri. In book: Carl Adam Petri: Ideas, Personality, Impact 2019: 193-204

  2018

• Artur Niewiadomski, Piotr Switalski, Teofil Sidoruk, Wojciech Penczek: SMT-Solvers in Action: Encoding and Solving Selected Problems in NP and EXPTIME. Sci. Ann. Comp. Sci. 28(2): 269-288 (2018)

• Artur Niewiadomski, Piotr Switalski, Marcin Kowalczyk, Wojciech Penczek: TripICS - a Web Service Composition System for Planning Trips and Travels. Fundam. Inform. 157(4): 403-425 (2018)

• Wojciech Jamroga, Wojciech Penczek, Piotr Dembinski, Antoni W. Mazurkiewicz: Towards Partial Order Reductions for Strategic Ability. AAMAS 2018: 156-165

• Artur Meski, Maciej Koutny, Wojciech Penczek: Reaction Mining for Reaction Systems. UCNC 2018: 131-144

  2017

• Artur Niewiadomski, Wojciech Penczek, Jaroslaw Skaruz, Maciej Szreter, Agata Pólrola. Combining ontology reductions with new approaches to automated abstract planning of Planics. Appl. Soft Comput. 53: 352-379, 2017

• Artur Meski, Maciej Koutny, Wojciech Penczek: Verification of Linear-Time Temporal Properties for Reaction Systems with Discrete Concentrations. Fundam. Inform. 154(1-4): 289-306 (2017)

• Étienne André, Laure Petrucci, Wojciech Jamroga, Michal Knapik, Wojciech Penczek. Timed ATL: Forget Memory, Just Count. AAMAS 2017: 1460-1462

  2016

• Piotr Dembiński, Wojciech Jamroga, Antoni Mazurkiewicz, Wojciech Penczek. Towards Partial Order Reductions for Fragments of Alternating-Time Temporal Logic. Report 1036, ICS PAS, December 2016

• Wojciech Jamroga, Beata Konikowska, Wojciech Penczek. Multi-Valued Verification of Strategic Ability. AAMAS 2016: 1180-1189

• Artur Meski, Maciej Koutny, Wojciech Penczek: Towards Quantitative Verification of Reaction Systems. UCNC 2016: 142-154
  Étienne André, Michal Knapik, Wojciech Penczek, Laure Petrucci: Controlling Actions and Time in Parametric Timed Automata. ACSD 2016: 45-54

  2015

• Michał Knapik, Artur Męski, Wojciech Penczek. Action Synthesis for Branching Time Logic: Theory and Applications. Transactions on Embedded Computing Systems 14(4):64, 2015

• Artur Męski, Wojciech Penczek, Grzegorz Rozenberg. Model checking temporal properties of reaction systems. Information Sciences 313, 22-42, 2015

• Alessio Lomuscio, Wojciech Penczek. Model Checking Temporal Epistemic Logic. pdf Chapter 8 of the Handbook of Epistemic Logic. H. van Ditmarsch, J. Halpern, W. van der Hoek, and B. Kooi (eds.). College Publications, pp. 397-441, 2015

• Artur Niewiadomski, Wojciech Penczek, Jarosław Skaruz. Hybrid Approach to Abstract Planning of Web Services.  Proceedings of The Seventh International Conferences on Advanced Service Computing: Service Computation, 35-40, 2015

  2014

• Artur Męski, Wojciech Penczek, Maciej Szreter, Bożena Woźna-Szcześniak, Andrzej Zbrzezny. BDD- versus SAT-based Bounded Model Checking for the Existential Fragment of Linear Temporal Logic with Knowledge: Algorithms and their Performance. Journal of Autonomous Agents and Multi-Agent Systems. Springer, 2014

• Artur Niewiadomski, Jarosław Skaruz, Wojciech Penczek, Maciej Szreter,  M. Jarocki: SMT Versus Genetic and OpenOpt Algorithms: Concrete Planning in the PlanICS Framework. Fundamenta Informaticae 135(4): 451-466 (2014)

• Artur Niewiadomski, Wojciech Penczek, Jarosław Skaruz. Combining Genetic Algorithm and SMT into Hybrid Approaches to Web Service Composition Problem. International Journal On Advances in Software, vol. 7 (3, 4): 675-685, 2014

  2013

• Agata Janowska, Wojciech Penczek, Agata Pólrola, Andrzej Zbrzezny. Using Integer Time Steps for Checking Branching Time Properties of Time Petri Nets. T. Petri Nets and Other Models of Concurrency 8: 89-105 (2013)

• Mariusz Jarocki, Artur Niewiadomski, Wojciech Penczek, Agata Półrola, Maciej Szreter. PlanICS 2.0 - a web service composition system, Advances in Software Development, Polish Information Processing Society I, 93 - 102, 2013

• Michal Knapik, Wojciech Penczek. Parameter Synthesis for Timed Kripke Structures. CEUR, CS&P 2013: 259-270

• Artur Niewiadomski, Wojciech Penczek, Jaroslaw Skaruz. SMT vs Genetic Algorithms: Concrete Planning in PlanICS Framework. CEUR, CS&P 2013: 309-321

• Jaroslaw Skaruz, Artur Niewiadomski, Wojciech Penczek. Automated abstract planning with use of genetic algorithms. GECCO (Companion), ACM 2013 ISBN 978-1-4503-1964-52013: 129-130

• Artur Niewiadomski, Wojciech Penczek. Towards SMT-based Abstract Planning in PlanICS Ontology, Proc. of the 5th International Conference on Knowledge Engineering and Ontology Development (KEOD 2013), pp. 123-131, (2013)

  2012

• Artur Niewiadomski, Wojciech Penczek, Agata, Maciej Szreter and Andrzej Zbrzezny. Towards Automatic Composition of Web Services: SAT-Based Concretisation of Abstract Scenarios, Fundam. Inform. 2012, 120(2), 181-203

• Dariusz Doliwa, Wojciech Horzelski, Mariusz Jarocki, Artur Niewiadomski, Wojciech Penczek, Agata Pólrola, Jaroslaw Skaruz. HarmonICS - a Tool for Composing Medical Services. ZEUS 2012: 25-33

• Michal Knapik, Wojciech Penczek. Bounded Model Checking for Parametric Timed Automata. T. Petri Nets and Other Models of Concurrency 5: 141-159, Springer-Verlag (2012)

• Andrew V. Jones, Michal Knapik, Wojciech Penczek, Alessio Lomuscio. Group synthesis for parametric temporal-epistemic logic. AAMAS 2012: 1107-1114

• Artur Meski, Wojciech Penczek, Maciej Szreter, Bozena Wozna-Szczesniak, Andrzej Zbrzezny: Bounded model checking for knowledge and linear time. AAMAS 2012: 1447-1448

• Artur Meski, Wojciech Penczek, Maciej Szreter. Bounded Model Checking for Linear Time Temporal-Epistemic Logic. ICCSW 2012: 88-94

• Artur Meski, Wojciech Penczek, Maciej Szreter, Bozena Wozna-Szczesniak, Andrzej Zbrzezny: Two Approaches to Bounded Model Checking for Linear Time Logic with Knowledge. KES-AMSTA 2012: 514-523, LNCS 7327.

  2011

• A. Męski, W. Penczek, A. Pólrola. BDD-based Bounded Model Checking for Temporal Properties of 1-Safe Petri Nets. Fundam. Inform. 109(3): 305-321 (2011)

• A. Lomuscio, W. Penczek, M. Solanki, Maciej Szreter. Runtime Monitoring of Contract Regulated Web Services. Fundam. Inform. 111(3): 339-355 (2011)

• D. Doliwa, W. Horzelski, M. Jarocki, A. Niewiadomski, W. Penczek, A. Pólrola, M. Szreter, A. Zbrzezny. PlanICS - a Web Service Composition Toolset. Fundam. Inform. 112(1): 47-71, 2011,

• Artur Męski, Agata Półrola, Wojciech Penczek, Bozena Wozna-Szczesniak, Andrzej Zbrzezny: Bounded Model Checking Approaches for Verification of Distributed Time Petri Nets. PNSE 2011: 72-91

• Wojciech Jamroga, Wojciech Penczek. Specification and Verification of Multi-Agent Systems. ESSLLI 2011: 210-263

  2010

• J. Lilius, W. Penczek: Applications and Theory of Petri Nets, 31st International Conference, PETRI NETS 2010, Braga, Portugal, June 21-25, 2010. Proceedings Springer 2010. book

• M. Jarocki, A. Niewiadomski, W. Penczek, A. Półrola, and M. Szreter, A Formal Approach to Composing Abstract Scenarios of Web Services, Proc. of IIS 2010, pp. 3 - 22, 2010. pdf

• M. A. Kłopotek, M. Marciniak, A. Mykowiecka, W. Penczek, S. T. Wierzchoń (Eds.) Conference proceedings , Intelligent Information Systems, 357 pages, ISBN 978-83-7051-580-5.

• A. Lomuscio, W. Penczek, M. Solanki, M. Szreter. Runtime monitoring of contract regulated web services. Proc. of the 9th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS10). Toronto, Canada. pp. 1149-1150, IFAAMAS Press. pdf

• A. Lomuscio, W. Penczek, H. Qu. Partial order reduction for model checking interleaved multi-agent systems. Proc. of the 9th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS10). Toronto, Canada. pp. 659-666. IFAAMAS Press. pdf

• M. Knapik, W. Penczek. Bounded Model Checking for Parametric Time Automata. Proc. of APNOC-SUMO Workshop, Braga, Portugal, 2010, pp. 45 - 60, pdf

• W. Penczek, A. Półrola, A. Zbrzezny. Towards Automatic Composition of Web Services: A SAT-based Phase, Proc. of APNOC-SUMO Workshop, Braga, Portugal, 2010, pp. 76 - 96, pdf

• A. Niewiadomski, W. Penczek, M. Szreter. Parametric Bounded Model Checking for UML, Proc. of APNOC-SUMO Workshop, Braga, Portugal, 2010, pp. 112 - 128, pdf

  2009

• G. Jakubowska, P. Dembiński, W. Penczek, M. Szreter, Simulation of Security Protocols based on Scenarios of Attacks, Fundamanta Informaticae, 2009, 93(1-3), 185-203. pdf

• M. Kurkowski, W. Penczek, Timed Automata Based Model Checking of Timed Security Protocols, Fundamanta Informaticae, 2009, 93(1-3), 245-259. pdf

• A. Lomuscio, W. Penczek, H. Qu, Towards Partial Order Reduction for Model Checking Temporal Epistemic Logic, Lecture Notes in Computer Science, Springer 2009, LNAI 5348, pp. 106-121. pdf

• A. Lomuscio, W. Penczek, H. Qu, Partial Order Reduction for Model Checking Interleaved Multi-agent Systems, Warsaw University 2009, Vol. II, Proc. of CS&P'09, pp. 361-372, pdf

• A Lomuscio, W. Penczek, M Solanki, M. Szreter, Runtime Monitoring of Contract Regulated Web Services, Warsaw University 2009, Vol. II, Proc. of CS&P'09, pp. 373-385.

• A. Niewiadomski, W. Penczek, M. Szreter, A New Approach to Model Checking of UML State Machines , Fundamanta Informaticae, 2009, 93(1-3), pp. 289-303. pdf

• A. Niewiadomski, W. Penczek, M. Szreter, Towards Checking Parametric Reachability for UML State Machines, Novosibirsk University 2009, Proc of. 7th International Andrei Ershov Memorial Conference Perspectives of System Informatics, pp. 229-240.

• A. Niewiadomski, W. Penczek, M. Szreter, Ograniczona Weryfikacja Modelowa Maszyn Stanowych UML, Systemy Czasu Rzeczywistego, Postępy badań i zastosowania, rozdz. 1, str. 13--22, ISBN 978-83-206-1746-7, Wydawnictwa Komunikacji i Łączności, Warszawa 2009.

• M. Knapik, M. Szreter, and W. Penczek, Bounded Parametric Model Checking for Elementary Net Systems, University of Hamburg, Department of Informatic 2009, Proc. of PNSE'09, pp. 97-118. pdf

• M. Kacprzak, W. Nabialek, A. Niewiadomski, W. Penczek, A. Polrola, M. Szreter, B. Wozna, and A. Zbrzezny, VerICS 2008 - a Model Checker for Time Petri Nets and High-Level Languages, University of Hamburg, Department of Informatics 2009, Proc. of PNSE'09, pp. 119-132. pdf

• W. Penczek, A. Półrola and A Zbrzezny, SAT-Based (Parametric) Reachability for Distributed Time Petri Nets 2009, University of Hamburg, Department of Informatics, Proc. of PNSE'09, pp. 133-156. pdf

• M. Knapik, W. Penczek, A. Półrola, Bounded Parametric Verication for Time Petri Nets with Discrete-Time Semantics Warsaw University 2009, Vol. I, Proc. of CS&P'09, pp. 277-290.

  2008

• A. Lomuscio, W. Penczek, LDYIS: a Framework for Model Checking Security Protocols, Fundamenta Informaticae, 2008, vol. 85, pp. 359 - 375. pdf

• M. Kacprzak, W. Nabiałek, A. Niewiadomski, W. Penczek, A. Półrola, M. Szreter, B. Woźna, A. Zbrzezny, Verics 2007 - a Model Checker for Knowledge and Real-Time, Fundamenta Informatiace, 2008, vol. 85, pp. 313-328. pdf

• M.Kacprzak, w. Nabiałek, A.Niewiadomski, W.Penczek, A.Półrola, M.Szreter, B.Woźna, A.Zbrzezny, "VerICS 2008 - a Model Checker for High-Level Languages", Proc. of Artificial Intelligence Studies AI2008, vol. 5(28) 2008, pp. 131-140.

• W. Penczek, M. Szreter, SAT-based Unbounded Model Checking of Timed Automata, Fundamenta Informaticae, 2008, vol. 85, pp. 425-440. pdf

• A. Niewiadomski, W. Penczek, M. Szreter, Towards Bounded Model Checking for UML Proceedings of Concurrency, Specification and Programming, Gross Vaeter See, 2008. pdf

• G. Jakubowska, W. Penczek, P. Dembinski, Simulation of Security Protocols based on Scenarios of Attacks, pp. 229 -241 Proceedings of Concurrency, Specification and Programming, Gross Vaeter See, 2008. pdf

• M. Kurkowski, W. Penczek, Verifying Timed Security Protocols via Translation to Timed Automata, pp. 289 - 301, Proceedings of Concurrency, Specification and Programming, Gross Vaeter See, 2008. pdf

• A. Niewiadomski, W.Penczek, M.Szreter, On Operational Semantics of UML State Machines, Proceedings of the 4th PDFCCS'08.

• A. Niewiadomski, W.Penczek, M.Szreter Semantyka operacyjna maszyn stanowych UML, Modele i zastosowania systemów czasu rzeczywistego, rozdz. 4., S. 45-54, ISBN 978-83-206-1702-3, wyd. Komunikacji i Łączności 2008, SCR 2008.

  2007

• M. Kacprzak, W. Nabiałek, A. Niewiadomski, W. Penczek, A. Półrola, M. Szreter, B. Woźna, A. Zbrzezny: VerICS 2006 - weryfikator dla systemów czasowych i wieloagentowych. . Mat. Konferencji Systemy Czasu Rzeczywistego (SCR'07), Rozdział , 2007.

• M. Kacprzak, W. Nabiałek, A. Niewiadomski, W. Penczek, Agata Półrola, M. Szreter, A. Zbrzezny, B. Woźna. VerICS 2006 - A Model Checker for Real-Time and Multi-Agent Systems. Proc. of CS&P'07, pp. 345-356, 2007. pdf

• A. Lomuscio, W. Penczek, B. Woźna, Bounded model checking for knowledge and real time, Artificial Intelligence 171 (2007) 1011-1038. pdf

• A. Lomuscio, W. Penczek: Logic Column 19: Symbolic Model Checking for Temporal-Epistemic Logics, in: ACM SIGACT News, Vol. 38 (3), 2007, pp. 77-99 pdf

• A Lomuscio, W. Penczek, Model Checking Security Protocols: A Multi-Agent System Approach, Proc. of CS&P'07, pp. 400-412, ISBN 978-83-88374-28-9, Warsaw University, Lagow, September 27-29, 2007. pdf

• G. Jakubowska, W. Penczek, Modelling and Checking Timed Authentication of Security Protocols, Fundamenta Informaticae, Vol. 79 No. 3-4, pp. 363 - 378, 2007. pdf

• G. Jakubowska, W. Penczek, Is your security protocol on time ?, F. Arbab and M. Sirjani (Eds.): FSEN 2007, LNCS 4767, pp. 65-80, 2007. pdf

• M. Kurkowski, W. Penczek, Verifying Security Protocols Modelled by Networks of Automata, Fundamenta Informaticae, Vol. 79 No. 3-4, pp. 453 - 471, 2007. pdf

• M. Kurkowski, W. Penczek, A. Zbrzezny, SAT-Based Verification of Security Protocols via Translation to Networks of Automata, S. Edelkamp and A. Lomuscio (Eds.): MoChart IV, LNAI 4428, pp. 146-165, 2007. pdf

• W. Penczek, M. Szreter, SAT-based Unbounded Model Checking of Timed Automata, Proc. of CS&P'07, pp. 451-462, 2007. pdf

• W. Penczek, M. Szreter, SAT-based Unbounded Model Checking of Timed Automata, ACSD'07, IEEE Computer Society 2007, pp. 236-237, 2007. pdf

• Janowska, W. Penczek, Path Compression in Timed Automata, Fundamenta Informaticae, Vol. 79 No. 3-4, str. 379 -399, 2007. pdf

  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, Fundamenta Informaticae, 2006. ps.gz

• B. Konikowska, W. Penczek, Model Checking for Multivalued Logic of Knowledge and Time, Proc. of AAMAS'06, ACM, 2006. pdf.gz

  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

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

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

  2004

• 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

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

• B. Wozna, A. Lomuscio, W. Penczek, Bounded model checking for knowledge over real time, Proc. of CSP'04, 2004, 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

• 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

• M. Kacprzak and W. Penczek, Model Checking for Alternating-Time mi-Calculus via Translation to SAT, Proc. of CSP'04, 2004, 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

• 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

• W. Penczek, A. Polrola, B. Wozna, A. Zbrzezny, Bounded Model Checking for Reachability Testing in Time Petri Nets, Proc. of CSP'04, 2004, pdf.gz

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

• B. Konikowska and W. Penczek, Model Checking Multi-Valued Modal Mi-Calculus: Revisited, Proc. of CS&P'04, 2004, 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

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

  2003

• M. Kacprzak, A. Lomuscio, and W. Penczek, Unbounded model checking for knowledge and time, Report 966, 2003, ps

• W. Penczek and A. Polrola, Minimization algorithms for Time Petri Nets, Proc. of CS&P'03, 2003, ps.gz

• B. Konikowska and W. Penczek, On designated values in multi-valued CTL* model checking, Proc. of CS&P'03, 2003, ps.gz

• M. Kacprzak, A. Lomuscio, and W. Penczek, Unbounded model checking for knowledge and time, Proc. of CS&P'03, 2003, ps.gz

• P. Dembinski, A. Janowska, P. Janowski, W. Penczek, 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

• A. Polrola, W. Penczek, and M. Szreter, Reachability Analysis for Timed Automata based on Partitioning, ICS PAS Report 961, 2003, ps.gz

• P. Dembinski, A. Janowska, P. Janowski, W. Penczek, 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

• A. Lomuscio, T. Lasica, and W. Penczek, Bounded Model Checking for interpreted systems: preliminary experimental results, Proc. of FAABS II, LNCS 2699, 2003. ps.gz

• A. Lomuscio and W. Penczek, Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking, Proc. of AAMAS'03, in T. Sandholm, editor, 2003. ps.gz

• M. Kacprzak, A. Lomuscio, and W. Penczek, 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

• W. Penczek, A. Polrola, and M. Szreter, Reachability Analysis for Timed Automata Using Partitioning Algorithms, Fundamenta Informaticae, Vol. 55(2), pp. 203-221, 2003, ps.gz

• A. Lomuscio and W. Penczek, Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking, Fundamenta Informaticae, Vol. 55(2), pp. 167-185, 2003, ps.gz

• W. Penczek, B. Wozna, and A. Zbrzezny, Checking Reachability Properties for Timed Automata via SAT, Fundamenta Informaticae, Vol. 55(2), pp. 223-241, 2003, ps.gz

  2002

• W. Pencze,k B. Wozna and A. Zbrzezny, Bounded Model Checking for the Universal fragment of CTL, Fundamenta Informaticae, 2002. ps.gz

• B. Konikowska and W. Penczek, Model Checking for Multi-Valued CTL*, a chapter in the book on Multi-Valued Logics, M. Fitting and E. Orlowska eds., 2002. ps.gz

• P. Dembinski, W. Penczek, and A. Polrola, Verification of Timed Automata Based on Similarity, Fundamenta Informaticae, 2002. PS.gz file - fi02-dpp.ps.gz

• W. Penczek, B. Wozna, and A. Zbrzezny, Bounded Model Checking for Elementary Nets Systems, ICS PAS Report 940, 2002. ps.gz

• B. Konikowska and W. Penczek, Reducing Model Checking from Multi-Valued CTL* to CTL*, Proc. of CONCUR'02, LNCS 2421, 2002. ps.gz

• W. Penczek, B. Wozna, and A. Zbrzezny, Towards Bounded Model Checking for the Universal Fragment of TCTL, Proc. of FTRTFT'02, LNCS 2469, 2002. ps.gz

• H. Hansen, W. Penczek, and A. Valmari, Stuttering-Insensitive Automata for On-the-fly Detection of Livelock Properties, Proc. of FMICS'02, 2002. ps.gz

• A. Lomuscio and W. Penczek, Bounded Model Checking for Interpreted Systems, ICS PAS Report 946, 2002. ps.gz

• W. Penczek, B. Wozna, and A. Zbrzezny, Towards Bounded Model Checking for the Universal Fragment of TCTL, ICS PAS Report 947, 2002. ps.gz

• W. Penczek, B. Wozna, and A. Zbrzezny, Checking Reachability Properties via SAT, ICS PAS Report 949, 2002. ps.gz

  2001

• S. Ambroszkiewicz, T. Nowak, and W. Penczek, 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

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

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

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

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

• P. Dembinski, W. Penczek, 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

  2000

• S. Ambroszkiewicz, K. Cetnarowicz, and W. Penczek, Modeling Agent Organizations. In Proc. Advances in Soft Computing, Bystra, Poland, June 12-16, 2000.

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

• W. Penczek, M. Szreter, R. Gerth, and R. Kuiper, Improving Partial Order Reductions for Universal Branching Time Properties, Fundamenta Informaticae 43, 2000. ps.gz

• W. Penczek and M. Szreter, More than one, less than all: Linear to Branching revisited, Proc. of CS\&P, Berlin, 2000.

• W. Penczek and M. Szreter, Automatyczna weryfikacja systemow czasu rzeczywistego, Proc. of SCR, Krak/ow, 2000. ps.gz

  1999

• S. Ambroszkiewicz and W. Penczek, 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

• S. Ambroszkiewicz and W. Penczek, Local interactions, explicit communication, and causal Knowledge in Games and Multi-Agent Systems. Proc. of CEEMAS'99, St. Petersburg, 1999. ps.gz

• R. Gerth, R. Kuiper, W. Penczek, and M. Szreter, Partial Order Reductions Preserving Simulations, Proc. of CSP'99, Warsaw, ps.gz

• R. Gerth, R. Kuiper, D. Peled, and W. Penczek, A partial order approach to branching time logic model-checking, Information and Computation, 1999. ps.gz

• S. Ambroszkiewicz and W. Penczek, 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

  1998

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

• S. Ambroszkiewicz, O. Matyja, and W. Penczek, Team formation in a distributed environment: the idea and algorithms, < IPI PAN, Report 855, 1998. ps.gz

• W. Penczek, Temporal logic of causal knowledge, Proc. of WoLLIC'98, pp. 178 - 187, Sau Paulo, 1998. ps.gz

• S. Ambroszkiewicz, O. Matyja, and W. Penczek, 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

• S. Ambroszkiewicz, O. Matyja, and W. Penczek, 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

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

  1997

• W. Penczek and M. Srebrny, 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

• W. Penczek, Model checking for a Fragment of Event Structures, Proceedings of TACAS'97, LNCS 1217, pp. 146--164, 1997. ps.gz

• R. Gerth, R. Kuiper, and W. Penczek, Partial Order Reductions Preserving Simulations, IPI PAN Raport 843, 1997. ps.gz

• S. Ambroszkiewicz and W. Penczek, 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

  1996

• D. Peled and W. Penczek, 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

• W. Penczek and A. Szałas, Proceedings of MFCS'96 (editors), LNCS 1113 , pp. 592, 1996.

• W. Penczek, Axiomatizations of Temporal Logics on Trace Systems, Fundamenta Informaticae 25, pp. 183--200, 1996. ps.gz

  1995

• R. Gerth, R. Kuiper, D. Peled, and W. Penczek, 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

• P. Niebert and W. Penczek, On the connection of partial order logics and partial order reductions, Raport TUE 95-15, Eindhoven University, 1995. ps.gz

• W. Penczek, 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

• R. Kuiper and W. Penczek, "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

• R. Alur, D. Peled, and W. Penczek, 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

  1994

• R. Kuiper and W. Penczek, 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.

• R. Kuiper and W. Penczek, 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.

• M. Kwiatkowska, D. Peled, and W. Penczek, 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

  1993

• W. Penczek, 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

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

  1992

• R. Kuiper, U. Goltz, and W. Penczek, Propositional temporal logics and equivalences, Proc. of International Conference on Concurrency Theory, LNCS 630, pp. 222-236, 1992. ps.gz

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

• W. Penczek, On undecidability of propositional temporal logics on trace systems, Information Processing Letters 43, pp. 147-153, 1992. ps.gz