Wojciech Penczek

196 papers A* 4A 23B 9C 7Misc 1Journal 93Unranked 51

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	IMITATOR4AMAS: Strategy Synthesis for STCTL. CoRR Davide Catta, Adrien Lacroix, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk
2026	J	`jnl`	Strategic (timed) computation tree logic. Auton. Agents Multi Agent Syst. Jaime Arias, Wojciech Jamroga, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk
2026	J	`jnl`	Towards Probabilistic Strategic Timed CTL. CoRR Wojciech Jamroga, Marta Kwiatkowska, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk
2025	—	`conf`	Formal Models are Magic. PNSE/ATAED/PeNGE@PETRI NETS Davide Catta, Wojciech Penczek, Laure Petrucci
2025	J	`jnl`	Model checking for distributed reaction systems with temporal-epistemic properties. Nat. Comput. Artur Meski, Maciej Koutny, Lukasz Mikulski, Ion Petre, Wojciech Penczek, Marcin Piatkowski
2025	A	`conf`	Practical Abstractions for Model Checking Continuous-Time Multi-Agent Systems. AAMAS Yan Kim, Wojciech Jamroga, Wojciech Penczek, Laure Petrucci
2025	J	`jnl`	Practical Abstractions for Model Checking Continuous-Time Multi-Agent Systems. CoRR Yan Kim, Wojciech Jamroga, Wojciech Penczek, Laure Petrucci
2025	A	`conf`	Probabilistic Timed ATL. AAMAS Wojciech Jamroga, Marta Kwiatkowska, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk
2025	—	`conf`	Satisfiability Checking for (Strategic) Timed CTL Using IMITATOR. ICAART (1) Wojciech Penczek, Laure Petrucci, Teofil Sidoruk
2024	J	`jnl`	Asynchronous Agents with Perfect Recall: Model Reductions, Knowledge-Based Construction, and Model Checking for Coalitional Strategies. CoRR Dilian Gurov, Filip Jamroga, Wojciech Jamroga, Mateusz Kaminski, Damian Kurpiewski, Wojciech Penczek, Teofil Sidoruk
2024	C	`conf`	Model Checking and Synthesis for Strategic Timed CTL using Strategies in Rewriting Logic. PPDP Jaime Arias, Carlos Olarte, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk
2024	J	`jnl`	Optimal Scheduling of Agents in ADTrees: Specialized Algorithm and Declarative Models. IEEE Trans. Reliab. Jaime Arias, Carlos Olarte, Laure Petrucci, Lukasz Masko, Wojciech Penczek, Teofil Sidoruk
2024	J	`jnl`	Reaction mining for reaction systems. Nat. Comput. Artur Meski, Maciej Koutny, Lukasz Mikulski, Wojciech Penczek
2024	A	`conf`	SMT4SMTL: A Tool for SMT-Based Satisfiability Checking of SMTL. AAMAS Artur Niewiadomski, Maciej Nazarczuk, Mateusz Przychodzki, Magdalena Kacprzak, Wojciech Penczek, Andrzej Zbrzezny
2023	—	`conf`	Model Checking of Strategic Timed Temporal Logics (Invited Talk). PNSE@Petri Nets Wojciech Penczek
2023	J	`jnl`	MsATL: a Tool for SAT-Based ATL Satisfiability Checking. CoRR Artur Niewiadomski, Magdalena Kacprzak, Damian Kurpiewski, Michal Knapik, Wojciech Penczek, Wojciech Jamroga
2023	J	`jnl`	Multi-Valued Verification of Strategic Ability. CoRR Wojciech Jamroga, Beata Konikowska, Damian Kurpiewski, Wojciech Penczek
2023	J	`jnl`	Optimal Scheduling of Agents in ADTrees: Specialised Algorithm and Declarative Models. CoRR Jaime Arias, Carlos Olarte, Laure Petrucci, Lukasz Masko, Wojciech Penczek, Teofil Sidoruk
2023	A	`conf`	SMT-Based Satisfiability Checking of Strategic Metric Temporal Logic. ECAI Magdalena Kacprzak, Artur Niewiadomski, Wojciech Penczek, Andrzej Zbrzezny
2023	A	`conf`	Strategic (Timed) Computation Tree Logic. AAMAS Jaime Arias, Wojciech Jamroga, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk
2023	J	`jnl`	Strategic (Timed) Computation Tree Logic. CoRR Jaime Arias, Wojciech Jamroga, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk
2023	J	`jnl`	Verification of Multi-Agent Properties in Electronic Voting: A Case Study. CoRR Damian Kurpiewski, Wojciech Jamroga, Lukasz Masko, Lukasz Mikulski, Witold Pazderski, Wojciech Penczek, Teofil Sidoruk
2022	B	`conf`	Minimal Schedule with Minimal Number of Agents in Attack-Defence Trees. ICECCS Jaime Arias, Laure Petrucci, Lukasz Masko, Wojciech Penczek, Teofil Sidoruk
2022	C	`conf`	Modular Analysis of Tree-Topology Models. ICFEM Jaime Arias, Michal Knapik, Wojciech Penczek, Laure Petrucci
2022	B	`conf`	Verification of Multi-Agent Properties in Electronic Voting: A Case Study. AiML Wojtek Jamroga, Lukasz Masko, Lukasz Mikulski, Witold Pazderski, Wojciech Penczek, Teofil Sidoruk, Damian Kurpiewski
2021	A	`conf`	ADT2AMAS: Managing Agents in Attack-Defence Scenarios. AAMAS Jaime Arias, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk
2021	J	`jnl`	Minimal Schedule with Minimal Number of Agents in Attack-Defence Trees. CoRR Jaime Arias, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk
2021	J	`jnl`	Preface. Fundam. Informaticae Jörg Keller, Wojciech Penczek
2021	J	`jnl`	Preface. Fundam. Informaticae Holger Schlingloff, Wojciech Penczek
2021	C	`conf`	SMT-Based Unbounded Model Checking for ATL. VECoS Michal Kanski, Artur Niewiadomski, Magdalena Kacprzak, Wojciech Penczek, Wojciech Nabialek
2021	A*	`conf`	Satisfiability Checking of Strategy Logic with Simple Goals. KR Magdalena Kacprzak, Artur Niewiadomski, Wojciech Penczek
2021	A*	`conf`	Strategic Abilities of Asynchronous Agents: Semantic Side Effects and How to Tame Them. KR Wojciech Jamroga, Wojciech Penczek, Teofil Sidoruk
2021	A	`conf`	Strategic Abilities of Asynchronous Agents: Semantic Side Effects. AAMAS Wojciech Jamroga, Wojciech Penczek, Teofil Sidoruk
2020	C	`conf`	Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-agent Systems. ICFEM Jaime Arias, Carlos E. Budde, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk, Mariëlle Stoelinga
2020	A	`conf`	MsATL: A Tool for SAT-Based ATL Satisfiability Checking. AAMAS Artur Niewiadomski, Magdalena Kacprzak, Damian Kurpiewski, Michal Knapik, Wojciech Penczek, Wojciech Jamroga
2020	J	`jnl`	Multi-valued Verification of Strategic Ability. Fundam. Informaticae Wojciech Jamroga, Beata Konikowska, Damian Kurpiewski, Wojciech Penczek
2020	A*	`conf`	SAT-Based ATL Satisfiability Checking. KR Magdalena Kacprzak, Artur Niewiadomski, Wojciech Penczek
2020	J	`jnl`	SAT-Based ATL Satisfiability Checking. CoRR Magdalena Kacprzak, Artur Niewiadomski, Wojciech Penczek
2020	J	`jnl`	Strategic Abilities of Asynchronous Agents: Semantic Paradoxes and How to Tame Them. CoRR Wojciech Jamroga, Wojciech Penczek, Teofil Sidoruk
2020	J	`jnl`	Towards Partial Order Reductions for Strategic Ability. J. Artif. Intell. Res. Wojciech Jamroga, Wojciech Penczek, Teofil Sidoruk, Piotr Dembinski, Antoni W. Mazurkiewicz
2019	—	`ch.`	All True Concurrency Models Start with Petri Nets: A Personal Tribute to Carl Adam Petri. Carl Adam Petri: Ideas, Personality, Impact Wojciech Penczek
2019	J	`jnl`	Applying Modern SAT-solvers to Solving Hard Problems. Fundam. Informaticae Artur Niewiadomski, Piotr Switalski, Teofil Sidoruk, Wojciech Penczek
2019	J	`jnl`	Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-Agent Systems. CoRR Jaime Arias, Carlos E. Budde, Wojciech Penczek, Laure Petrucci, Mariëlle Stoelinga
2019	J	`jnl`	Parametric Verification: An Introduction. CoRR Étienne André, Michal Knapik, Didier Lime, Wojciech Penczek, Laure Petrucci
2019	J	`jnl`	Parametric Verification: An Introduction. Trans. Petri Nets Other Model. Concurr. Étienne André, Michal Knapik, Didier Lime, Wojciech Penczek, Laure Petrucci
2019	J	`jnl`	Preface. Fundam. Informaticae Victor Khomenko, Jetty Kleijn, Wojciech Penczek, Olivier H. Roux
2019	J	`jnl`	Preface. Fundam. Informaticae Wojciech Penczek, Holger Schlingloff, Piotr Wasilewski
2019	B	`conf`	Squeezing State Spaces of (Attack-Defence) Trees. ICECCS Laure Petrucci, Michal Knapik, Wojciech Penczek, Teofil Sidoruk
2019	J	`jnl`	Timed ATL: Forget Memory, Just Count. J. Artif. Intell. Res. Michal Knapik, Étienne André, Laure Petrucci, Wojciech Jamroga, Wojciech Penczek
2018	C	`ed.`	25th International Symposium on Temporal Representation and Reasoning, TIME 2018, Warsaw, Poland, October 15-17, 2018 TIME Natasha Alechina, Kjetil Nørvåg, Wojciech Penczek
2018	—	`conf`	Improving Efficiency of Model Checking for Variants of Alternating-time Temporal Logic. CS&P Wojciech Penczek
2018	J	`jnl`	Preface. Fundam. Informaticae Wil M. P. van der Aalst, Eike Best, Wojciech Penczek
2018	J	`jnl`	Preface. Fundam. Informaticae Ludwik Czaja, Wojciech Penczek, Holger Schlingloff, Hung Son Nguyen
2018	—	`conf`	Reaction Mining for Reaction Systems. UCNC Artur Meski, Maciej Koutny, Wojciech Penczek
2018	J	`jnl`	SMT-Solvers in Action: Encoding and Solving Selected Problems in NP and EXPTIME. Sci. Ann. Comput. Sci. Artur Niewiadomski, Piotr Switalski, Teofil Sidoruk, Wojciech Penczek
2018	A	`conf`	Towards Partial Order Reductions for Strategic Ability. AAMAS Wojciech Jamroga, Wojciech Penczek, Piotr Dembinski, Antoni W. Mazurkiewicz
2018	—	`ed.`	Transactions on Petri Nets and Other Models of Concurrency XIII Trans. Petri Nets and Other Models of Concurrency Maciej Koutny, Lars Michael Kristensen, Wojciech Penczek
2018	J	`jnl`	TripICS - a Web Service Composition System for Planning Trips and Travels. Fundam. Informaticae Artur Niewiadomski, Piotr Switalski, Marcin Kowalczyk, Wojciech Penczek
2017	J	`jnl`	Combining ontology reductions with new approaches to automated abstract planning of Planics. Appl. Soft Comput. Artur Niewiadomski, Wojciech Penczek, Jaroslaw Skaruz, Maciej Szreter, Agata Pólrola
2017	A	`conf`	Timed ATL: Forget Memory, Just Count. AAMAS Étienne André, Laure Petrucci, Wojciech Jamroga, Michal Knapik, Wojciech Penczek
2017	—	`ed.`	Transactions on Petri Nets and Other Models of Concurrency XII Trans. Petri Nets and Other Models of Concurrency Maciej Koutny, Jetty Kleijn, Wojciech Penczek
2017	J	`jnl`	Verification of Linear-Time Temporal Properties for Reaction Systems with Discrete Concentrations. Fundam. Informaticae Artur Meski, Maciej Koutny, Wojciech Penczek
2016	—	`book`	Challenging Problems and Solutions in Intelligent Systems Challenging Problems and Solutions in Intelligent Systems Guy De Tré, Przemyslaw Grzegorzewski, Janusz Kacprzyk, Jan W. Owsinski, Wojciech Penczek, Slawomir Zadrozny
2016	J	`jnl`	Concrete Planning in PlanICS Framework by Combining SMT with GEO and Simulated Annealing. Fundam. Informaticae Artur Niewiadomski, Jaroslaw Skaruz, Piotr Switalski, Wojciech Penczek
2016	—	`conf`	Controlling Actions and Time in Parametric Timed Automata. ACSD Étienne André, Michal Knapik, Wojciech Penczek, Laure Petrucci
2016	A	`conf`	Multi-Valued Verification of Strategic Ability. AAMAS Wojciech Jamroga, Beata Konikowska, Wojciech Penczek
2016	J	`jnl`	Preface. Fundam. Informaticae Ludwik Czaja, Wojciech Penczek, Krzysztof Stencel
2016	J	`jnl`	Preface. Fundam. Informaticae Ludwik Czaja, Wojciech Penczek, Krzysztof Stencel
2016	J	`jnl`	Preface. Fundam. Informaticae Raymond Devillers, Antti Valmari, Wojciech Penczek
2016	—	`ch.`	SMT-Based Parameter Synthesis for Parametric Timed Automata. Challenging Problems and Solutions in Intelligent Systems Michal Knapik, Wojciech Penczek
2016	—	`conf`	Towards Quantitative Verification of Reaction Systems. UCNC Artur Meski, Maciej Koutny, Wojciech Penczek
2016	—	`conf`	TripICS - a Web Service Composition System for Planning Trips and Travels (extended abstract). CS&P Artur Niewiadomski, Wojciech Penczek
2015	J	`jnl`	Action Synthesis for Branching Time Logic: Theory and Applications. ACM Trans. Embed. Comput. Syst. Michal Knapik, Artur Meski, Wojciech Penczek
2015	B	`conf`	Generating None-Plans in Order to Find Plans. SEFM Michal Knapik, Artur Niewiadomski, Wojciech Penczek
2015	—	`conf`	Hybrid Planning by Combining SMT and Simulated Annealing. CS&P Jaroslaw Skaruz, Artur Niewiadomski, Wojciech Penczek
2015	J	`jnl`	Model checking temporal properties of reaction systems. Inf. Sci. Artur Meski, Wojciech Penczek, Grzegorz Rozenberg
2015	J	`jnl`	SMT-Based Abstract Parametric Temporal Planning. Trans. Petri Nets Other Model. Concurr. Artur Niewiadomski, Wojciech Penczek
2014	—	`conf`	A Hybrid Approach to Web Service Composition Problem in the PlanICS Framework. MobiWIS Artur Niewiadomski, Wojciech Penczek, Jaroslaw Skaruz
2014	—	`conf`	Action Synthesis for Branching Time Logic: Theory and Applications. ACSD Michal Knapik, Artur Meski, Wojciech Penczek
2014	J	`jnl`	BDD-versus SAT-based bounded model checking for the existential fragment of linear temporal logic with knowledge: algorithms and their performance. Auton. Agents Multi Agent Syst. Artur Meski, Wojciech Penczek, Maciej Szreter, Bozena Wozna-Szczesniak, Andrzej Zbrzezny
2014	—	`conf`	Fixed-Point Methods in Parametric Model Checking. IEEE Conf. on Intelligent Systems (1) Michal Knapik, Wojciech Penczek
2014	J	`jnl`	Parameter Synthesis for Timed Kripke Structures. Fundam. Informaticae Michal Knapik, Wojciech Penczek
2014	—	`conf`	PlanICS 2.0 - A Tool for Composing Services. PNSE @ Petri Nets Artur Niewiadomski, Wojciech Penczek
2014	J	`jnl`	Preface. Fundam. Informaticae Wojciech Penczek, Ludwik Czaja
2014	J	`jnl`	SMT Versus Genetic and OpenOpt Algorithms: Concrete Planning in the PlanICS Framework. Fundam. Informaticae Artur Niewiadomski, Jaroslaw Skaruz, Wojciech Penczek, Maciej Szreter, Mariusz Jarocki
2014	—	`conf`	SMT-based Abstract Temporal Planning. PNSE @ Petri Nets Artur Niewiadomski, Wojciech Penczek
2013	—	`conf`	Automated abstract planning with use of genetic algorithms. GECCO (Companion) Jaroslaw Skaruz, Artur Niewiadomski, Wojciech Penczek
2013	—	`conf`	Evolutionary Algorithms for Abstract Planning. PPAM (1) Jaroslaw Skaruz, Artur Niewiadomski, Wojciech Penczek
2013	—	`conf`	Parameter Synthesis for Timed Kripke Structures. CS&P Michal Knapik, Wojciech Penczek
2013	J	`jnl`	Preface. Fundam. Informaticae Lars Michael Kristensen, Wojciech Penczek, Laure Petrucci
2013	—	`conf`	SMT vs Genetic Algorithms: Concrete Planning in PlanICS Framework. CS&P Artur Niewiadomski, Wojciech Penczek, Jaroslaw Skaruz
2013	C	`conf`	Towards SMT-based Abstract Planning in PlanICS Ontology. KEOD Artur Niewiadomski, Wojciech Penczek
2013	J	`jnl`	Using Integer Time Steps for Checking Branching Time Properties of Time Petri Nets. Trans. Petri Nets Other Model. Concurr. Agata Janowska, Wojciech Penczek, Agata Pólrola, Andrzej Zbrzezny
2012	—	`ch.`	Applying Timed Automata to Model Checking of Security Protocols. Handbook of Finite State Based Models and Applications Miroslaw Kurkowski, Wojciech Penczek
2012	—	`conf`	Bounded Model Checking for Linear Time Temporal-Epistemic Logic. ICCSW Artur Meski, Wojciech Penczek, Maciej Szreter
2012	J	`jnl`	Bounded Model Checking for Parametric Timed Automata. Trans. Petri Nets Other Model. Concurr. Michal Knapik, Wojciech Penczek
2012	A	`conf`	Bounded model checking for knowledge and linear time. AAMAS Artur Meski, Wojciech Penczek, Maciej Szreter, Bozena Wozna-Szczesniak, Andrzej Zbrzezny
2012	A	`conf`	Group synthesis for parametric temporal-epistemic logic. AAMAS Andrew V. Jones, Michal Knapik, Wojciech Penczek, Alessio Lomuscio
2012	—	`conf`	HarmonICS - a Tool for Composing Medical Services. ZEUS Dariusz Doliwa, Wojciech Horzelski, Mariusz Jarocki, Artur Niewiadomski, Wojciech Penczek, Agata Pólrola, Jaroslaw Skaruz
2012	J	`jnl`	Preface. Fundam. Informaticae Wojciech Penczek
2012	—	`conf`	SMT-based parameter synthesis for L/U automata. PNSE Michal Knapik, Wojciech Penczek
2012	—	`conf`	Symbolic Model Checking for Temporal-Epistemic Logic. Logic Programs, Norms and Action Alessio Lomuscio, Wojciech Penczek
2012	J	`jnl`	Towards Automatic Composition of Web Services: SAT-Based Concretisation of Abstract Scenarios. Fundam. Informaticae Artur Niewiadomski, Wojciech Penczek, Agata Pólrola, Maciej Szreter, Andrzej Zbrzezny
2012	J	`jnl`	Towards SAT-based BMC for LTLK over Interleaved Interpreted Systems. Fundam. Informaticae Wojciech Penczek, Bozena Wozna-Szczesniak, Andrzej Zbrzezny
2012	—	`conf`	Two Approaches to Bounded Model Checking for Linear Time Logic with Knowledge. KES-AMSTA Artur Meski, Wojciech Penczek, Maciej Szreter, Bozena Wozna-Szczesniak, Andrzej Zbrzezny
2012	—	`conf`	Using Integer Time Steps for Checking Branching Time Properties of Time Petri Nets. PNSE Agata Janowska, Wojciech Penczek, Agata Pólrola, Andrzej Zbrzezny
2011	J	`jnl`	BDD-based Bounded Model Checking for Temporal Properties of 1-Safe Petri Nets. Fundam. Informaticae Artur Meski, Wojciech Penczek, Agata Pólrola
2011	—	`conf`	Bounded Model Checking Approaches for Verification of Distributed Time Petri Nets. PNSE Artur Meski, Agata Pólrola, Wojciech Penczek, Bozena Wozna-Szczesniak, Andrzej Zbrzezny
2011	J	`jnl`	PlanICS - a Web Service Composition Toolset. Fundam. Informaticae Dariusz Doliwa, Wojciech Horzelski, Mariusz Jarocki, Artur Niewiadomski, Wojciech Penczek, Agata Pólrola, Maciej Szreter, Andrzej Zbrzezny
2011	J	`jnl`	Preface. Fundam. Informaticae Johan Lilius, Wojciech Penczek
2011	J	`jnl`	Preface. Fundam. Informaticae Wojciech Penczek
2011	J	`jnl`	Runtime Monitoring of Contract Regulated Web Services. Fundam. Informaticae Alessio Lomuscio, Wojciech Penczek, Monika Solanki, Maciej Szreter
2011	—	`conf`	Specification and Verification of Multi-Agent Systems. ESSLLI Wojciech Jamroga, Wojciech Penczek
2010	B	`ed.`	Applications and Theory of Petri Nets, 31st International Conference, PETRI NETS 2010, Braga, Portugal, June 21-25, 2010. Proceedings Petri Nets Johan Lilius, Wojciech Penczek
2010	—	`conf`	Bounded Model Checking for Parametric Timed Automata. ACSD/Petri Nets Workshops Michal Knapik, Wojciech Penczek
2010	J	`jnl`	Bounded Parametric Model Checking for Elementary Net Systems. Trans. Petri Nets Other Model. Concurr. Michal Knapik, Maciej Szreter, Wojciech Penczek
2010	J	`jnl`	Bounded Parametric Verification for Distributed Time Petri Nets with Discrete-Time Semantics. Fundam. Informaticae Michal Knapik, Wojciech Penczek, Maciej Szreter, Agata Pólrola
2010	J	`jnl`	Parametric Model Checking with VerICS. Trans. Petri Nets Other Model. Concurr. Michal Knapik, Artur Niewiadomski, Wojciech Penczek, Agata Pólrola, Maciej Szreter, Andrzej Zbrzezny
2010	J	`jnl`	Partial Order Reductions for Model Checking Temporal-epistemic Logics over Interleaved Multi-agent Systems. Fundam. Informaticae Alessio Lomuscio, Wojciech Penczek, Hongyang Qu
2010	A	`conf`	Partial order reductions for model checking temporal epistemic logics over interleaved multi-agent systems. AAMAS Alessio Lomuscio, Wojciech Penczek, Hongyang Qu
2010	J	`jnl`	Preface. Fundam. Informaticae Giuliana Franceschinis, Wojciech Penczek, Karsten Wolf
2010	J	`jnl`	Preface. Fundam. Informaticae Wojciech Penczek
2010	A	`conf`	Runtime monitoring of contract regulated web services. AAMAS Alessio Lomuscio, Monika Solanki, Wojciech Penczek, Maciej Szreter
2010	J	`jnl`	SAT-Based (Parametric) Reachability for a Class of Distributed Time Petri Nets. Trans. Petri Nets Other Model. Concurr. Wojciech Penczek, Agata Pólrola, Andrzej Zbrzezny
2010	—	`conf`	Towards Automatic Composition of Web Services: A SAT-Based Phase. ACSD/Petri Nets Workshops Wojciech Penczek, Agata Pólrola, Andrzej Zbrzezny
2009	J	`jnl`	A New Approach to Model Checking of UML State Machines. Fundam. Informaticae Artur Niewiadomski, Wojciech Penczek, Maciej Szreter
2009	J	`jnl`	Simulation of Security Protocols based on Scenarios of Attacks. Fundam. Informaticae Gizela Jakubowska, Piotr Dembinski, Wojciech Penczek, Maciej Szreter
2009	J	`jnl`	Timed Automata Based Model Checking of Timed Security Protocols. Fundam. Informaticae Miroslaw Kurkowski, Wojciech Penczek
2009	—	`conf`	Towards Checking Parametric Reachability for UML State Machines. Ershov Memorial Conference Artur Niewiadomski, Wojciech Penczek, Maciej Szreter
2008	J	`jnl`	LDYIS: a Framework for Model Checking Security Protocols. Fundam. Informaticae Alessio Lomuscio, Wojciech Penczek
2008	J	`jnl`	SAT-based Unbounded Model Checking of Timed Automata. Fundam. Informaticae Wojciech Penczek, Maciej Szreter
2008	—	`conf`	Towards Partial Order Reduction for Model Checking Temporal Epistemic Logic. MoChArt Alessio Lomuscio, Wojciech Penczek, Hongyang Qu
2008	J	`jnl`	VerICS 2007 - a Model Checker for Knowledge and Real-Time. Fundam. Informaticae Magdalena Kacprzak, Wojciech Nabialek, Artur Niewiadomski, Wojciech Penczek, Agata Pólrola, Maciej Szreter, Bozena Wozna, Andrzej Zbrzezny
2007	J	`jnl`	Bounded model checking for knowledge and real time. Artif. Intell. Alessio Lomuscio, Wojciech Penczek, Bozena Wozna
2007	—	`conf`	Is Your Security Protocol on Time ? FSEN Gizela Jakubowska, Wojciech Penczek
2007	J	`jnl`	Logic Column 19: Symbolic Model Checking for Temporal-Epistemic Logics CoRR Alessio Lomuscio, Wojciech Penczek
2007	J	`jnl`	Modelling and Checking Timed Authentication of Security Protocols. Fundam. Informaticae Gizela Jakubowska, Wojciech Penczek
2007	J	`jnl`	Path Compression in Timed Automata. Fundam. Informaticae Agata Janowska, Wojciech Penczek
2007	—	`conf`	SAT-based Unbounded Model Checking of Timed Automata. ACSD Wojciech Penczek, Maciej Szreter
2007	J	`jnl`	Symbolic model checking for temporal-epistemic logics. SIGACT News Alessio Lomuscio, Wojciech Penczek
2007	J	`jnl`	Verifying Security Protocols Modelled by Networks of Automata. Fundam. Informaticae Miroslaw Kurkowski, Wojciech Penczek
2006	—	`book`	Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach. Wojciech Penczek, Agata Pólrola
2006	J	`jnl`	Comparing BDD and SAT Based Techniques for Model Checking Chaum's Dining Cryptographers Protocol. Fundam. Informaticae Magdalena Kacprzak, Alessio Lomuscio, Artur Niewiadomski, Wojciech Penczek, Franco Raimondi, Maciej Szreter
2006	A	`conf`	Model checking for multivalued logic of knowledge and time. AAMAS Beata Konikowska, Wojciech Penczek
2006	—	`conf`	SAT-Based Verification of Security Protocols Via Translation to Networks of Automata. MoChArt Miroslaw Kurkowski, Wojciech Penczek, Andrzej Zbrzezny
2005	A	`conf`	Bounded model checking for knowledge and real time. AAMAS Bozena Wozna, Alessio Lomuscio, Wojciech Penczek
2005	J	`jnl`	Fully Symbolic Unbounded Model Checking for Alternating-time Temporal Logic Auton. Agents Multi Agent Syst. Magdalena Kacprzak, Wojciech Penczek
2004	J	`jnl`	A Sat-Based Approach to Unbounded Model Checking for Alternating-Time Temporal Epistemic Logic. Synth. Magdalena Kacprzak, Wojciech Penczek
2004	—	`conf`	Bounded Model Checking for Deontic Interpreted Systems. LCMAS Bozena Wozna, Alessio Lomuscio, Wojciech Penczek
2004	J	`jnl`	From Bounded to Unbounded Model Checking for Temporal Epistemic Logic. Fundam. Informaticae Magdalena Kacprzak, Alessio Lomuscio, Wojciech Penczek
2004	J	`jnl`	Minimization Algorithms for Time Petri Nets. Fundam. Informaticae Agata Pólrola, Wojciech Penczek
2004	J	`jnl`	On Designated Values in Multi-valued CTL Fundam. Informaticae Beata Konikowska, Wojciech Penczek
2004	—	`conf`	Specification and Model Checking of Temporal Properties in Time Petri Nets and Timed Automata. ICATPN Wojciech Penczek, Agata Pólrola
2004	A	`conf`	Unbounded Model Checking for Alternating-Time Temporal Logic. AAMAS Magdalena Kacprzak, Wojciech Penczek
2004	A	`conf`	Verification of Multiagent Systems via Unbounded Model Checking. AAMAS Magdalena Kacprzak, Alessio Lomuscio, Wojciech Penczek
2004	—	`conf`	Verifying Multi-agent Systems via Unbounded Model Checking. FAABS Magdalena Kacprzak, Alessio Lomuscio, T. Lasica, Wojciech Penczek, Maciej Szreter
2003	J	`jnl`	Checking Reachability Properties for Timed Automata via SAT. Fundam. Informaticae Bozena Wozna, Andrzej Zbrzezny, Wojciech Penczek
2003	J	`jnl`	Reachability Analysis for Timed Automata Using Partitioning Algorithms. Fundam. Informaticae Agata Pólrola, Wojciech Penczek, Maciej Szreter
2003	—	`conf`	Towards Efficient Partition Refinement for Checking Reachability in Timed Automata. FORMATS Agata Pólrola, Wojciech Penczek, Maciej Szreter
2003	A	`conf`	Verics: A Tool for Verifying Timed Automata and Estelle Specifications. TACAS Piotr Dembinski, Agata Janowska, Pawel Janowski, Wojciech Penczek, Agata Pólrola, Maciej Szreter, Bozena Wozna, Andrzej Zbrzezny
2003	J	`jnl`	Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking. Fundam. Informaticae Wojciech Penczek, Alessio Lomuscio
2003	A	`conf`	Verifying epistemic properties of multi-agent systems via bounded model checking. AAMAS Wojciech Penczek, Alessio Lomuscio
2002	—	`conf`	Bounded Model Checking for Interpreted Systems: Preliminary Experimental Results. FAABS Alessio Lomuscio, T. Lasica, Wojciech Penczek
2002	J	`jnl`	Bounded Model Checking for the Universal Fragment of CTL. Fundam. Informaticae Wojciech Penczek, Bozena Wozna, Andrzej Zbrzezny
2002	B	`conf`	Reducing Model Checking from Multi-valued {\rm CTL}^{\ast} to {\rm CTL}^{\ast}. CONCUR Beata Konikowska, Wojciech Penczek
2002	C	`conf`	Stuttering-Insensitive Automata for On-the-fly Detection of Livelock Properties. FMICS Henri Hansen, Wojciech Penczek, Antti Valmari
2002	—	`conf`	Towards Bounded Model Checking for the Universal Fragment of TCTL. FTRTFT Wojciech Penczek, Bozena Wozna, Andrzej Zbrzezny
2002	J	`jnl`	Verification of Timed Automata Based on Similarity. Fundam. Informaticae Piotr Dembinski, Wojciech Penczek, Agata Pólrola
2001	—	`conf`	Abstractions and Partial Order Reductions for Checking Branching Properties of Time Petri Nets. ICATPN Wojciech Penczek, Agata Pólrola
2001	Misc	`conf`	Automated Verification of Infinite State Concurrent Systems. PPAM Piotr Dembinski, Wojciech Penczek, Agata Pólrola
2001	—	`conf`	Efficient Model Checking of Causal-Knowledge Protocols. CEEMAS Wojciech Penczek
2000	J	`jnl`	Improving Partial Order Reductions for Universal Branching Time Properties. Fundam. Informaticae Wojciech Penczek, Maciej Szreter, Rob Gerth, Ruurd Kuiper
2000	—	`conf`	Modeling Agent Organizations. Intelligent Information Systems Stanislaw Ambroszkiewicz, Krzysztof Cetnarowicz, Jaroslaw Kozlak, Tomasz Nowak, Wojciech Penczek
2000	J	`jnl`	Temporal Approach to Causal Knowledge. Log. J. IGPL Wojciech Penczek
2000	—	`conf`	Towards Formal Specification and Verification in Cyberspace. FAABS Stanislaw Ambroszkiewicz, Wojciech Penczek, Tomasz Nowak
1999	J	`jnl`	A Partial Order Approach to Branching Time Logic Model Checking. Inf. Comput. Rob Gerth, Ruurd Kuiper, Doron A. Peled, Wojciech Penczek
1999	—	`conf`	Local Interactions, Explicit Communication and Causal Knowledge in Games and Multi-Agent Systems. CEEMAS Stanislaw Ambroszkiewicz, Wojciech Penczek
1999	—	`conf`	Model checking of causal knowledge formulas. WDS@FCT Wojciech Penczek, Stanislaw Ambroszkiewicz
1998	—	`conf`	Team Formation by Self-Interested Mobile Agents. DAI Stanislaw Ambroszkiewicz, Olaf Matyja, Wojciech Penczek
1997	A	`conf`	Model-Checking for a Subclass of Event Structures. TACAS Wojciech Penczek
1996	—	`conf`	A complete axiomatization of a first-order temporal logic over trace systems. Partial Order Methods in Verification Wojciech Penczek, Marian Srebrny
1996	J	`jnl`	Axiomatizations of Temporal Logics on Trace Systems. Fundam. Informaticae Wojciech Penczek
1996	B	`ed.`	Mathematical Foundations of Computer Science 1996, 21st International Symposium, MFCS'96, Cracow, Poland, September 2-6, 1996, Proceedings MFCS Wojciech Penczek, Andrzej Szalas
1995	—	`conf`	A Partial Order Approach to Branching Time Logic Model Checking. ISTCS Rob Gerth, Ruurd Kuiper, Doron A. Peled, Wojciech Penczek
1995	A*	`conf`	Model-Checking of Causality Properties LICS Rajeev Alur, Doron A. Peled, Wojciech Penczek
1995	—	`ch.`	Traces and Logic. The Book of Traces Wojciech Penczek, Ruurd Kuiper
1995	—	`conf`	Using asynchronous Büchi automata for efficient automatic verification of concurrent systems. PSTV Doron A. Peled, Wojciech Penczek
1994	—	`conf`	A Hierarchy of Partial Order Temporal Properties. ICTL Marta Z. Kwiatkowska, Doron A. Peled, Wojciech Penczek
1993	A	`conf`	Axiomatizations of Temporal Logics on Trace Systems. STACS Wojciech Penczek
1993	J	`jnl`	Temporal Logics for Trace Systems: On Automated Verification. Int. J. Found. Comput. Sci. Wojciech Penczek
1992	J	`jnl`	On Undecidability of Propositional Temporal Logics on Trace Systems. Inf. Process. Lett. Wojciech Penczek
1992	B	`conf`	Propositional Temporal Logics and Equivalences. CONCUR Ursula Goltz, Ruurd Kuiper, Wojciech Penczek
1990	J	`jnl`	Inevitability in diamond processes. RAIRO Theor. Informatics Appl. Edward Ochmanski, Wojciech Penczek
1989	B	`conf`	A Concurrent Branching Time Temporal Logic. CSL Wojciech Penczek
1989	—	`conf`	A Temporal Logic for the Local Specification of Concurrent Systems. IFIP Congress Wojciech Penczek
1989	J	`jnl`	Concurrent Systems and Inevitability. Theor. Comput. Sci. Antoni W. Mazurkiewicz, Edward Ochmanski, Wojciech Penczek