Wojciech Penczek

Orcid: 0000-0001-6477-4863

According to our database1, Wojciech Penczek authored at least 155 papers between 1989 and 2023.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2023
Optimal Scheduling of Agents in ADTrees: Specialised Algorithm and Declarative Models.
CoRR, 2023

SMT-Based Satisfiability Checking of Strategic Metric Temporal Logic.
Proceedings of the ECAI 2023 - 26th European Conference on Artificial Intelligence, September 30 - October 4, 2023, Kraków, Poland, 2023

Strategic (Timed) Computation Tree Logic.
Proceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems, 2023

Model Checking of Strategic Timed Temporal Logics (Invited Talk).
Proceedings of the 2023 International Workshop on Petri Nets and Software Engineering (PNSE 2023) co-located with the 44th International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS 2023), 2023

2022
Modular Analysis of Tree-Topology Models.
Proceedings of the Formal Methods and Software Engineering, 2022

Minimal Schedule with Minimal Number of Agents in Attack-Defence Trees.
Proceedings of the 26th International Conference on Engineering of Complex Computer Systems, 2022

Verification of Multi-Agent Properties in Electronic Voting: A Case Study.
Proceedings of the Advances in Modal Logic, AiML 2022, Rennes, France, 2022

2021
Preface.
Fundam. Informaticae, 2021

Preface.
Fundam. Informaticae, 2021

Minimal Schedule with Minimal Number of Agents in Attack-Defence Trees.
CoRR, 2021

SMT-Based Unbounded Model Checking for ATL.
Proceedings of the Verification and Evaluation of Computer and Communication Systems, 2021

Satisfiability Checking of Strategy Logic with Simple Goals.
Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning, 2021

Strategic Abilities of Asynchronous Agents: Semantic Side Effects and How to Tame Them.
Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning, 2021

Strategic Abilities of Asynchronous Agents: Semantic Side Effects.
Proceedings of the AAMAS '21: 20th International Conference on Autonomous Agents and Multiagent Systems, 2021

ADT2AMAS: Managing Agents in Attack-Defence Scenarios.
Proceedings of the AAMAS '21: 20th International Conference on Autonomous Agents and Multiagent Systems, 2021

2020
Towards Partial Order Reductions for Strategic Ability.
J. Artif. Intell. Res., 2020

Multi-valued Verification of Strategic Ability.
Fundam. Informaticae, 2020

Strategic Abilities of Asynchronous Agents: Semantic Paradoxes and How to Tame Them.
CoRR, 2020

SAT-Based ATL Satisfiability Checking.
Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, 2020

Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-agent Systems.
Proceedings of the Formal Methods and Software Engineering, 2020

MsATL: A Tool for SAT-Based ATL Satisfiability Checking.
Proceedings of the 19th International Conference on Autonomous Agents and Multiagent Systems, 2020

2019
Parametric Verification: An Introduction.
Trans. Petri Nets Other Model. Concurr., 2019

Timed ATL: Forget Memory, Just Count.
J. Artif. Intell. Res., 2019

Preface.
Fundam. Informaticae, 2019

Applying Modern SAT-solvers to Solving Hard Problems.
Fundam. Informaticae, 2019

Preface.
Fundam. Informaticae, 2019

Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-Agent Systems.
CoRR, 2019

Squeezing State Spaces of (Attack-Defence) Trees.
Proceedings of the 24th International Conference on Engineering of Complex Computer Systems, 2019

All True Concurrency Models Start with Petri Nets: A Personal Tribute to Carl Adam Petri.
Proceedings of the Carl Adam Petri: Ideas, Personality, Impact, 2019

2018
TripICS - a Web Service Composition System for Planning Trips and Travels.
Fundam. Informaticae, 2018

Preface.
Fundam. Informaticae, 2018

Preface.
Fundam. Informaticae, 2018

SMT-Solvers in Action: Encoding and Solving Selected Problems in NP and EXPTIME.
Sci. Ann. Comput. Sci., 2018

Reaction Mining for Reaction Systems.
Proceedings of the Unconventional Computation and Natural Computation, 2018

Improving Efficiency of Model Checking for Variants of Alternating-time Temporal Logic.
Proceedings of the 27th International Workshop on Concurrency, 2018

Towards Partial Order Reductions for Strategic Ability.
Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, 2018

2017
Verification of Linear-Time Temporal Properties for Reaction Systems with Discrete Concentrations.
Fundam. Informaticae, 2017

Combining ontology reductions with new approaches to automated abstract planning of Planics.
Appl. Soft Comput., 2017

2016
SMT-Based Parameter Synthesis for Parametric Timed Automata.
Proceedings of the Challenging Problems and Solutions in Intelligent Systems, 2016

Concrete Planning in PlanICS Framework by Combining SMT with GEO and Simulated Annealing.
Fundam. Informaticae, 2016

Preface.
Fundam. Informaticae, 2016

Preface.
Fundam. Informaticae, 2016

Towards Quantitative Verification of Reaction Systems.
Proceedings of the Unconventional Computation and Natural Computation, 2016

TripICS - a Web Service Composition System for Planning Trips and Travels (extended abstract).
Proceedings of the 25th International Workshop on Concurrency, 2016

Multi-Valued Verification of Strategic Ability.
Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems, 2016

Controlling Actions and Time in Parametric Timed Automata.
Proceedings of the 16th International Conference on Application of Concurrency to System Design, 2016

2015
SMT-Based Abstract Parametric Temporal Planning.
Trans. Petri Nets Other Model. Concurr., 2015

Action Synthesis for Branching Time Logic: Theory and Applications.
ACM Trans. Embed. Comput. Syst., 2015

Model checking temporal properties of reaction systems.
Inf. Sci., 2015

Generating None-Plans in Order to Find Plans.
Proceedings of the Software Engineering and Formal Methods - 13th International Conference, 2015

Hybrid Planning by Combining SMT and Simulated Annealing.
Proceedings of the 24th International Workshop on Concurrency, 2015

2014
Preface.
Fundam. Informaticae, 2014

SMT Versus Genetic and OpenOpt Algorithms: Concrete Planning in the PlanICS Framework.
Fundam. Informaticae, 2014

Parameter Synthesis for Timed Kripke Structures.
Fundam. Informaticae, 2014

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., 2014

A Hybrid Approach to Web Service Composition Problem in the PlanICS Framework.
Proceedings of the Mobile Web Information Systems - 11th International Conference, 2014

Fixed-Point Methods in Parametric Model Checking.
Proceedings of the Intelligent Systems'2014, 2014

PlanICS 2.0 - A Tool for Composing Services.
Proceedings of the International Workshop on Petri Nets and Software Engineering, 2014

SMT-based Abstract Temporal Planning.
Proceedings of the International Workshop on Petri Nets and Software Engineering, 2014

2013
Using Integer Time Steps for Checking Branching Time Properties of Time Petri Nets.
Trans. Petri Nets Other Model. Concurr., 2013

Preface.
Fundam. Informaticae, 2013

Evolutionary Algorithms for Abstract Planning.
Proceedings of the Parallel Processing and Applied Mathematics, 2013

Towards SMT-based Abstract Planning in PlanICS Ontology.
Proceedings of the KEOD 2013, 2013

Automated abstract planning with use of genetic algorithms.
Proceedings of the Genetic and Evolutionary Computation Conference, 2013

SMT vs Genetic Algorithms: Concrete Planning in PlanICS Framework.
Proceedings of the 22nd International Workshop on Concurrency, 2013

2012
Applying Timed Automata to Model Checking of Security Protocols.
Proceedings of the Handbook of Finite State Based Models and Applications., 2012

Bounded Model Checking for Parametric Timed Automata.
Trans. Petri Nets Other Model. Concurr., 2012

Towards SAT-based BMC for LTLK over Interleaved Interpreted Systems.
Fundam. Informaticae, 2012

Preface.
Fundam. Informaticae, 2012

Towards Automatic Composition of Web Services: SAT-Based Concretisation of Abstract Scenarios.
Fundam. Informaticae, 2012

HarmonICS - a Tool for Composing Medical Services.
Proceedings of the 4<sup>th</sup> Central-European Workshop on Services and their Composition, 2012

Two Approaches to Bounded Model Checking for Linear Time Logic with Knowledge.
Proceedings of the Agent and Multi-Agent Systems. Technologies and Applications, 2012

Bounded Model Checking for Linear Time Temporal-Epistemic Logic.
Proceedings of the 2012 Imperial College Computing Student Workshop, 2012

Symbolic Model Checking for Temporal-Epistemic Logic.
Proceedings of the Logic Programs, Norms and Action, 2012

SMT-based parameter synthesis for L/U automata.
Proceedings of the International Workshop on Petri Nets and Software Engineering, 2012

Bounded model checking for knowledge and linear time.
Proceedings of the International Conference on Autonomous Agents and Multiagent Systems, 2012

Group synthesis for parametric temporal-epistemic logic.
Proceedings of the International Conference on Autonomous Agents and Multiagent Systems, 2012

2011
BDD-based Bounded Model Checking for Temporal Properties of 1-Safe Petri Nets.
Fundam. Informaticae, 2011

Runtime Monitoring of Contract Regulated Web Services.
Fundam. Informaticae, 2011

Preface.
Fundam. Informaticae, 2011

PlanICS - a Web Service Composition Toolset.
Fundam. Informaticae, 2011

Specification and Verification of Multi-Agent Systems.
Proceedings of the Lectures on Logic and Computation, 2011

Bounded Model Checking Approaches for Verification of Distributed Time Petri Nets.
Proceedings of the International Workshop on Petri Nets and Software Engineering, 2011

2010
SAT-Based (Parametric) Reachability for a Class of Distributed Time Petri Nets.
Trans. Petri Nets Other Model. Concurr., 2010

Bounded Parametric Model Checking for Elementary Net Systems.
Trans. Petri Nets Other Model. Concurr., 2010

Parametric Model Checking with VerICS.
Trans. Petri Nets Other Model. Concurr., 2010

Partial Order Reductions for Model Checking Temporal-epistemic Logics over Interleaved Multi-agent Systems.
Fundam. Informaticae, 2010

Bounded Parametric Verification for Distributed Time Petri Nets with Discrete-Time Semantics.
Fundam. Informaticae, 2010

Preface.
Fundam. Informaticae, 2010

Towards Automatic Composition of Web Services: A SAT-Based Phase.
Proceedings of the Workshops of the 31st International Conference on Application and Theory of Petri Nets and Other Models of Concurrency (PETRI NETS 2010) and of the 10th International Conference on Application of Concurrency to System Design (ACSD 2010), 2010

2009
A New Approach to Model Checking of UML State Machines.
Fundam. Informaticae, 2009

Timed Automata Based Model Checking of Timed Security Protocols.
Fundam. Informaticae, 2009

Simulation of Security Protocols based on Scenarios of Attacks.
Fundam. Informaticae, 2009

Towards Checking Parametric Reachability for UML State Machines.
Proceedings of the Perspectives of Systems Informatics, 2009

2008
SAT-based Unbounded Model Checking of Timed Automata.
Fundam. Informaticae, 2008

LDYIS: a Framework for Model Checking Security Protocols.
Fundam. Informaticae, 2008

VerICS 2007 - a Model Checker for Knowledge and Real-Time.
Fundam. Informaticae, 2008

Towards Partial Order Reduction for Model Checking Temporal Epistemic Logic.
Proceedings of the Model Checking and Artificial Intelligence, 5th International Workshop, 2008

2007
Symbolic model checking for temporal-epistemic logics.
SIGACT News, 2007

Verifying Security Protocols Modelled by Networks of Automata.
Fundam. Informaticae, 2007

Path Compression in Timed Automata.
Fundam. Informaticae, 2007

Modelling and Checking Timed Authentication of Security Protocols.
Fundam. Informaticae, 2007

Logic Column 19: Symbolic Model Checking for Temporal-Epistemic Logics
CoRR, 2007

Bounded model checking for knowledge and real time.
Artif. Intell., 2007

Is Your Security Protocol on Time ?
Proceedings of the International Symposium on Fundamentals of Software Engineering, 2007

2006
Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach.
Studies in Computational Intelligence 20, Springer, ISBN: 978-3-540-32869-8, 2006

Comparing BDD and SAT Based Techniques for Model Checking Chaum's Dining Cryptographers Protocol.
Fundam. Informaticae, 2006

SAT-Based Verification of Security Protocols Via Translation to Networks of Automata.
Proceedings of the Model Checking and Artificial Intelligence, 4th Workshop, 2006

Model checking for multivalued logic of knowledge and time.
Proceedings of the 5th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2006), 2006

2005
Fully Symbolic Unbounded Model Checking for Alternating-time Temporal Logic<sup>1</sup>.
Auton. Agents Multi Agent Syst., 2005

2004
A Sat-Based Approach to Unbounded Model Checking for Alternating-Time Temporal Epistemic Logic.
Synth., 2004

Minimization Algorithms for Time Petri Nets.
Fundam. Informaticae, 2004

On Designated Values in Multi-valued CTL<sup>*</sup> Model Checking.
Fundam. Informaticae, 2004

From Bounded to Unbounded Model Checking for Temporal Epistemic Logic.
Fundam. Informaticae, 2004

Bounded Model Checking for Deontic Interpreted Systems.
Proceedings of the 2nd International Workshop on Logic and Communication in Multi-Agent Systems, 2004

Verifying Multi-agent Systems via Unbounded Model Checking.
Proceedings of the Formal Approaches to Agent-Based Systems, Third InternationalWorkshop, 2004

Unbounded Model Checking for Alternating-Time Temporal Logic.
Proceedings of the 3rd International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2004), 2004

Verification of Multiagent Systems via Unbounded Model Checking.
Proceedings of the 3rd International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2004), 2004

Specification and Model Checking of Temporal Properties in Time Petri Nets and Timed Automata.
Proceedings of the Applications and Theory of Petri Nets 2004, 2004

2003
Checking Reachability Properties for Timed Automata via SAT.
Fundam. Informaticae, 2003

Reachability Analysis for Timed Automata Using Partitioning Algorithms.
Fundam. Informaticae, 2003

Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking.
Fundam. Informaticae, 2003

Verics: A Tool for Verifying Timed Automata and Estelle Specifications.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2003

Towards Efficient Partition Refinement for Checking Reachability in Timed Automata.
Proceedings of the Formal Modeling and Analysis of Timed Systems: First International Workshop, 2003

2002
Bounded Model Checking for the Universal Fragment of CTL.
Fundam. Informaticae, 2002

Verification of Timed Automata Based on Similarity.
Fundam. Informaticae, 2002

Stuttering-Insensitive Automata for On-the-fly Detection of Livelock Properties.
Proceedings of the 7th International ERCIM Workshop in Formal Methods for Industrial Critical Systems, 2002

Towards Bounded Model Checking for the Universal Fragment of TCTL.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 2002

Bounded Model Checking for Interpreted Systems: Preliminary Experimental Results.
Proceedings of the Formal Approaches to Agent-Based Systems, Second International Workshop, 2002

Reducing Model Checking from Multi-valued {\rm CTL}^{\ast} to {\rm CTL}^{\ast}.
Proceedings of the CONCUR 2002, 2002

2001
Automated Verification of Infinite State Concurrent Systems.
Proceedings of the Parallel Processing and Applied Mathematics, 2001

Efficient Model Checking of Causal-Knowledge Protocols.
Proceedings of the From Theory to Practice in Multi-Agent Systems, 2001

Abstractions and Partial Order Reductions for Checking Branching Properties of Time Petri Nets.
Proceedings of the Application and Theory of Petri Nets 2001, 2001

2000
Temporal Approach to Causal Knowledge.
Log. J. IGPL, 2000

Improving Partial Order Reductions for Universal Branching Time Properties.
Fundam. Informaticae, 2000

Modeling Agent Organizations.
Proceedings of the Intelligent Information Systems, 2000

Towards Formal Specification and Verification in Cyberspace.
Proceedings of the Formal Approaches to Agent-Based Systems, First International Workshop, 2000

1999
A Partial Order Approach to Branching Time Logic Model Checking.
Inf. Comput., 1999

Model checking of causal knowledge formulas.
Proceedings of the Workshop on Distributed Systems, 1999

Local Interactions, Explicit Communication and Causal Knowledge in Games and Multi-Agent Systems.
Proceedings of the 1st International Workshop of Central and Eastern Europe on Multi-Agent Systems, 1999

1998
Team Formation by Self-Interested Mobile Agents.
Proceedings of the Multi-Agent Systems: Theories, 1998

1997
Model-Checking for a Subclass of Event Structures.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1997

1996
Axiomatizations of Temporal Logics on Trace Systems.
Fundam. Informaticae, 1996

A complete axiomatization of a first-order temporal logic over trace systems.
Proceedings of the Partial Order Methods in Verification, Proceedings of a DIMACS Workshop, 1996

1995
Using asynchronous Büchi automata for efficient automatic verification of concurrent systems.
Proceedings of the Protocol Specification, 1995

Model-Checking of Causality Properties
Proceedings of the Proceedings, 1995

Traces and Logic.
Proceedings of the Book of Traces, 1995

1994
A Hierarchy of Partial Order Temporal Properties.
Proceedings of the Temporal Logic, First International Conference, 1994

1993
Temporal Logics for Trace Systems: On Automated Verification.
Int. J. Found. Comput. Sci., 1993

1992
On Undecidability of Propositional Temporal Logics on Trace Systems.
Inf. Process. Lett., 1992

Propositional Temporal Logics and Equivalences.
Proceedings of the CONCUR '92, 1992

1990
Inevitability in diamond processes.
RAIRO Theor. Informatics Appl., 1990

1989
Concurrent Systems and Inevitability.
Theor. Comput. Sci., 1989

A Temporal Logic for the Local Specification of Concurrent Systems.
Proceedings of the Information Processing 89, Proceedings of the IFIP 11th World Computer Congress, San Francisco, USA, August 28, 1989

A Concurrent Branching Time Temporal Logic.
Proceedings of the CSL '89, 1989


  Loading...