Javier Esparza

Orcid: 0000-0001-9862-4919

Affiliations:
  • TU Munich, Faculty of Computer Science


According to our database1, Javier Esparza authored at least 227 papers between 1989 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Efficient Normalization of Linear Temporal Logic.
J. ACM, April, 2024

Fast and succinct population protocols for Presburger arithmetic.
J. Comput. Syst. Sci., March, 2024

Separators in Continuous Petri Nets.
Log. Methods Comput. Sci., 2024

Validity of contextual formulas (extended version).
CoRR, 2024

A Resolution-Based Interactive Proof System for UNSAT.
Proceedings of the Foundations of Software Science and Computation Structures, 2024

Validity of Contextual Formulas.
Proceedings of the 35th International Conference on Concurrency Theory, 2024

Computing Inductive Invariants of Regular Abstraction Frameworks.
Proceedings of the 35th International Conference on Concurrency Theory, 2024

2023
Lower bounds on the state complexity of population protocols.
Distributed Comput., September, 2023

Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy.
Log. Methods Comput. Sci., 2023

Making IP=PSPACE Practical: Efficient Interactive Protocols for BDD Algorithms.
CoRR, 2023

Black-Box Testing Liveness Properties of Partially Observable Stochastic Systems.
Proceedings of the 50th International Colloquium on Automata, Languages, and Programming, 2023

Geometry of Reachability Sets of Vector Addition Systems.
Proceedings of the 34th International Conference on Concurrency Theory, 2023

Making sf IP=sf PSPACE Practical: Efficient Interactive Protocols for BDD Algorithms.
Proceedings of the Computer Aided Verification - 35th International Conference, 2023

2022
Examples for submission to CONCUR'22.
Dataset, April, 2022

Examples for submission to CONCUR'22.
Dataset, April, 2022

From linear temporal logic and limit-deterministic Büchi automata to deterministic parity automata.
Int. J. Softw. Tools Technol. Transf., 2022

Computing Parameterized Invariants of Parameterized Petri Nets.
Fundam. Informaticae, 2022

Regular Model Checking Upside-Down: An Invariant-Based Approach.
Proceedings of the 33rd International Conference on Concurrency Theory, 2022

A Simple Rewrite System for the Normalization of Linear Temporal Logic.
Proceedings of the Principles of Systems Design, 2022

2021
The 2021 Alonzo Church award for outstanding contributions to logic and computation: call for nominations.
ACM SIGLOG News, 2021

Towards efficient verification of population protocols.
Formal Methods Syst. Des., 2021

TheoretiCS.
Bull. EATCS, 2021

2021 Alonzo Church Award for Outstanding Contributions to Logic and Computation.
Bull. EATCS, 2021

The complexity of verifying population protocols.
Distributed Comput., 2021

Abduction of trap invariants in parameterized systems.
Proceedings of the Proceedings 12th International Symposium on Games, 2021

Back to the Future: A Fresh Look at Linear Temporal Logic.
Proceedings of the Implementation and Application of Automata, 2021

Population Protocols: Beyond Runtime Analysis.
Proceedings of the Reachability Problems - 15th International Conference, 2021

Decision Power of Weak Asynchronous Models of Distributed Computing.
Proceedings of the PODC '21: ACM Symposium on Principles of Distributed Computing, 2021

Lower Bounds on the State Complexity of Population Protocols.
Proceedings of the PODC '21: ACM Symposium on Principles of Distributed Computing, 2021

State Complexity of Population Protocols (Invited Talk).
Proceedings of the 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2021

Enforcing ω-Regular Properties in Markov Chains by Restarting.
Proceedings of the 32nd International Conference on Concurrency Theory, 2021

Verification.
Proceedings of the Handbook of Automata Theory., 2021

2020





ostrich.
Dataset, February, 2020

ostrich.
Dataset, February, 2020

A Unified Translation of Linear Temporal Logic to ω-Automata.
J. ACM, 2020

Online Monitoring ω-Regular Properties in Unknown Markov Chains.
CoRR, 2020

Structural Invariants for the Verification of Systems with Parameterized Architectures.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

Succinct Population Protocols for Presburger Arithmetic.
Proceedings of the 37th International Symposium on Theoretical Aspects of Computer Science, 2020

An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata.
Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

Flatness and Complexity of Immediate Observation Petri Nets.
Proceedings of the 31st International Conference on Concurrency Theory, 2020

A Classification of Weak Asynchronous Models of Distributed Computing.
Proceedings of the 31st International Conference on Concurrency Theory, 2020

Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

Peregrine 2.0: Explaining Correctness of Population Protocols Through Stage Graphs.
Proceedings of the Automated Technology for Verification and Analysis, 2020

Complexity of Verification and Synthesis of Threshold Automata.
Proceedings of the Automated Technology for Verification and Analysis, 2020

2019
Expressive Power of Oblivious Consensus Protocols.
CoRR, 2019

Negotiation as concurrency primitive.
Acta Informatica, 2019

Computing the Expected Execution Time of Probabilistic Workflow Nets.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Expressive Power of Broadcast Consensus Protocols.
Proceedings of the 30th International Conference on Concurrency Theory, 2019

Parameterized Analysis of Immediate Observation Petri Nets.
Proceedings of the Application and Theory of Petri Nets and Concurrency, 2019

Coffee and Cigarettes.
Proceedings of the Carl Adam Petri: Ideas, Personality, Impact, 2019

2018
Model Checking Procedural Programs.
Proceedings of the Handbook of Model Checking., 2018

Soundness in negotiations.
Log. Methods Comput. Sci., 2018

Alonzo Church Award 2018 - Call for Nominations.
Bull. EATCS, 2018

Formal Methods and Fault-Tolerant Distributed Comp.: Forging an Alliance (Dagstuhl Seminar 18211).
Dagstuhl Reports, 2018

Preface for the special issue GandALF 2015.
Acta Informatica, 2018

Computing the Concurrency Threshold of Sound Free-Choice Workflow Nets.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Large Flocks of Small Birds: on the Minimal Size of Population Protocols.
Proceedings of the 35th Symposium on Theoretical Aspects of Computer Science, 2018

One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Black Ninjas in the Dark: Formal Analysis of Population Protocols.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Verification of Immediate Observation Population Protocols.
Proceedings of the 29th International Conference on Concurrency Theory, 2018

Automatic Analysis of Expected Termination Time for Population Protocols.
Proceedings of the 29th International Conference on Concurrency Theory, 2018

Peregrine: A Tool for the Analysis of Population Protocols.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

2017
Minimizing Test Suites with Unfoldings of Multithreaded Programs.
ACM Trans. Embed. Comput. Syst., 2017

Polynomial analysis algorithms for free choice Probabilistic Workflow Nets.
Perform. Evaluation, 2017

Model checking parameterized asynchronous shared-memory systems.
Formal Methods Syst. Des., 2017

Quantitative Implementation Strategies for Safety Controllers.
CoRR, 2017

Verification of population protocols.
Acta Informatica, 2017

Advances in Quantitative Analysis of Free-Choice Workflow Petri Nets (Invited Talk).
Proceedings of the 24th International Symposium on Temporal Representation and Reasoning, 2017

From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Static analysis of deterministic negotiations.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

Advances in Parameterized Verification of Population Protocols.
Proceedings of the Computer Science - Theory and Applications, 2017

2016
Parameterized Verification of Crowds of Anonymous Processes.
Proceedings of the Dependable Software Systems Engineering, 2016

Negotiations and Petri Nets.
Trans. Petri Nets Other Model. Concurr., 2016

Parameterized Verification of Asynchronous Shared-Memory Systems.
J. ACM, 2016

Existence of home states in Petri nets is decidable.
Inf. Process. Lett., 2016

From LTL to deterministic automata - A safraless compositional approach.
Formal Methods Syst. Des., 2016

Model Checking Population Protocols.
Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2016

Reduction Rules for Colored Workflow Nets.
Proceedings of the Fundamental Approaches to Software Engineering, 2016

Limit-Deterministic Büchi Automata for Linear Temporal Logic.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015
FPSOLVE: A Generic Solver for Fixpoint Equations Over Semirings.
Int. J. Found. Comput. Sci., 2015

Distributed Markov Chains.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2015

An SMT-based Approach to Fair Termination Analysis.
Proceedings of the Formal Methods in Computer-Aided Design, 2015

Negotiation Programs.
Proceedings of the Application and Theory of Petri Nets and Concurrency, 2015

Unfolding Based Minimal Test Suites for Testing Multithreaded Programs.
Proceedings of the 15th International Conference on Application of Concurrency to System Design, 2015

2014
Pattern-Based Verification for Multithreaded Programs.
ACM Trans. Program. Lang. Syst., 2014

Reachability Problems for Infinite-State Systems (Dagstuhl Seminar 14141).
Dagstuhl Reports, 2014

Negotiation Games.
CoRR, 2014

Keeping a Crowd Safe: On the Complexity of Parameterized Verification (Corrected version).
CoRR, 2014

A Fully Verified Executable LTL Model Checker.
Arch. Formal Proofs, 2014

Message-Passing Algorithms for the Verification of Distributed Protocols.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2014

Keeping a Crowd Safe: On the Complexity of Parameterized Verification (Invited Talk).
Proceedings of the 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014), 2014

A Brief History of Strahler Numbers.
Proceedings of the Language and Automata Theory and Applications, 2014

On Negotiation as Concurrency Primitive II: Deterministic Cyclic Negotiations.
Proceedings of the Foundations of Software Science and Computation Structures, 2014

Fast and Accurate Unlexicalized Parsing via Structural Annotations.
Proceedings of the 14th Conference of the European Chapter of the Association for Computational Linguistics, 2014

Deterministic Negotiations: Concurrency for Free.
Proceedings of the CONCUR 2014 - Concurrency Theory - 25th International Conference, 2014

An SMT-Based Approach to Coverability Analysis.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

From LTL to Deterministic Automata: A Safraless Compositional Approach.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013
A strongly polynomial algorithm for criticality of branching processes and consistency of stochastic context-free grammars.
Inf. Process. Lett., 2013

Analyzing probabilistic pushdown automata.
Formal Methods Syst. Des., 2013

Computation of Summaries Using Net Unfoldings.
Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2013

On Negotiation as Concurrency Primitive.
Proceedings of the CONCUR 2013 - Concurrency Theory - 24th International Conference, 2013

2012
Space-efficient scheduling of stochastically generated tasks.
Inf. Comput., 2012

A Perfect Model for Bounded Verification.
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

Deterministic Automata for the (F, G)-Fragment of LTL.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

Proving Termination of Probabilistic Programs Using Patterns.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

Rabinizer: Small Deterministic Automata for LTL(F, G).
Proceedings of the Automated Technology for Verification and Analysis, 2012

Reactive and Proactive Diagnosis of Distributed Systems Using Net Unfoldings.
Proceedings of the 12th International Conference on Application of Concurrency to System Design, 2012

Three Case Studies on Verification of Infinite-State Systems.
Proceedings of the Modern Applications of Automata Theory., 2012

2011
Derivation tree analysis for accelerated fixed-point computation.
Theor. Comput. Sci., 2011

Parikhʼs theorem: A simple and direct automaton construction.
Inf. Process. Lett., 2011

Learning Workflow Petri Nets.
Fundam. Informaticae, 2011

Probabilistic Abstractions with Arbitrary Domains.
Proceedings of the Static Analysis - 18th International Symposium, 2011

Complexity of pattern-based verification for multithreaded programs.
Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Solving Fixed-Point Equations by Derivation Tree Analysis.
Proceedings of the Algebra and Coalgebra in Computer Science, 2011

2010
Newtonian Program Analysis - An Introduction.
Proceedings of the Logics and Languages for Reliability and Security, 2010

Computing the Least Fixed Point of Positive Polynomial Systems.
SIAM J. Comput., 2010

Newtonian program analysis.
J. ACM, 2010

Parikh's Theorem: A simple and direct construction
CoRR, 2010

Analysis of Systems with Stochastic Process Creation.
Proceedings of the Verification, 2010

Computing Least Fixed Points of Probabilistic Systems of Polynomials.
Proceedings of the 27th International Symposium on Theoretical Aspects of Computer Science, 2010

A False History of True Concurrency: From Petri to Tools.
Proceedings of the Model Checking Software, 2010

Verification of Graph Transformation Systems with Context-Free Specifications.
Proceedings of the Graph Transformations - 5th International Conference, 2010

Automatic Error Correction of Java Programs.
Proceedings of the Formal Methods for Industrial Critical Systems, 2010

2009
FTOS-Verify: Analysis and Verification of Non-Functional Properties for Fault-Tolerant Systems
CoRR, 2009

On least fixed points of systems of positive polynomials.
ACM Commun. Comput. Algebra, 2009

Stochastic Process Creation.
Proceedings of the Mathematical Foundations of Computer Science 2009, 2009

On the Memory Consumption of Probabilistic Pushdown Automata.
Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2009

Solving Fixed-Point Equations on omega-Continuous Semirings.
Proceedings of the 6th Workshop on Fixed Points in Computer Science, 2009

Modeling and Verification for Timing Satisfaction of Fault-Tolerant Systems with Finiteness.
Proceedings of the 13th IEEE/ACM International Symposium on Distributed Simulation and Real Time Applications, 2009

Examining robotic systems with shape-adjustable manipulators under dynamic environments: From simulation to verification.
Proceedings of the IEEE International Symposium on Computational Intelligence in Robotics and Automation, 2009

2008
Unfoldings - A Partial-Order Approach to Model Checking
Monographs in Theoretical Computer Science. An EATCS Series, Springer, ISBN: 978-3-540-77426-6, 2008

A negative result on depth-first net unfoldings.
Int. J. Softw. Tools Technol. Transf., 2008

Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems.
J. Satisf. Boolean Model. Comput., 2008

On the Complexity of Consistency and Complete State Coding for Signal Transition Graphs.
Fundam. Informaticae, 2008

SDSIrep: A Reputation System Based on SDSI.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

Convergence Thresholds of Newton's Method for Monotone Polynomial Equations.
Proceedings of the STACS 2008, 2008

Symbolic Context-Bounded Analysis of Multithreaded Java Programs.
Proceedings of the Model Checking Software, 2008

Solving Monotone Polynomial Equations.
Proceedings of the Fifth IFIP International Conference On Theoretical Computer Science, 2008

Newton's Method for omega-Continuous Semirings.
Proceedings of the Automata, Languages and Programming, 35th International Colloquium, 2008

Approximative Methods for Monotone Systems of Min-Max-Polynomial Equations.
Proceedings of the Automata, Languages and Programming, 35th International Colloquium, 2008

2007
On the convergence of Newton's method for monotone systems of polynomial equations.
Proceedings of the 39th Annual ACM Symposium on Theory of Computing, 2007

On Fixed Point Equations over Commutative Semirings.
Proceedings of the STACS 2007, 2007

An Extension of Newton's Method to <i>omega</i> -Continuous Semirings.
Proceedings of the Developments in Language Theory, 11th International Conference, 2007

jMoped: A Test Environment for Java Programs.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006
Model Checking Probabilistic Pushdown Automata.
Log. Methods Comput. Sci., 2006

Rewriting Models of Boolean Programs.
Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006

Separability in Conflict-Free Petri Nets.
Proceedings of the Perspectives of Systems Informatics, 2006

Reachability analysis of multithreaded software with asynchronous communication.
Proceedings of the Software Verification: Infinite-State Model Checking and Static Program Analysis, 19.02., 2006

Efficient Algorithms for Alternating Pushdown Systems with an Application to the Computation of Certificate Chains.
Proceedings of the Automated Technology for Verification and Analysis, 2006

Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols.
Proceedings of the Automated Technology for Verification and Analysis, 2006

2005
jMoped: A Java Bytecode Checker Based on Moped.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

A Note on On-the-Fly Verification Algorithms.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Locality-Based Abstractions.
Proceedings of the Static Analysis, 12th International Symposium, 2005

Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances.
Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 2005

Analysis and Prediction of the Long-Run Behavior of Probabilistic Sequential Programs with Recursion (Extended Abstract).
Proceedings of the 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2005), 2005

2004
A Polynomial-Time Algorithm for Checking Consistency of Free-Choice Signal Transition Graphs.
Fundam. Informaticae, 2004

Reachability Analysis of Synchronized PA Systems.
Proceedings of the 6th International Workshop on Verification of Infinite-State Systems, 2004

Verifying Probabilistic Procedural Programs.
Proceedings of the FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 2004

2003
A Logical Viewpoint on Process-algebraic Quotients.
J. Log. Comput., 2003

A Generic Approach to the Static Analysis of Concurrent Programs with Procedures.
Int. J. Found. Comput. Sci., 2003

Model checking LTL with regular valuations for pushdown systems.
Inf. Comput., 2003

Simple Representative Instantiations for Multicast Protocols.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2003

An Automata-Theoretic Approach to Software Verification.
Proceedings of the Developments in Language Theory, 7th International Conference, 2003

Synthesis of Distributed Algorithms Using Asynchronous Automata.
Proceedings of the CONCUR 2003, 2003

The Model-Checking Kit.
Proceedings of the Applications and Theory of Petri Nets 2003, 2003

2002
An Improvement of McMillan's Unfolding Algorithm.
Formal Methods Syst. Des., 2002

An Algebraic Approach to the Static Analysis of Concurrent Software.
Proceedings of the Static Analysis, 9th International Symposium, 2002

Grammars as Processes.
Proceedings of the Formal and Natural Computing, 2002

2001
Unfolding Based Algorithms for the Reachability Problem.
Fundam. Informaticae, 2001

Implementing LTL Model Checking with Net Unfoldings.
Proceedings of the Model Checking Software, 2001

Model Checking (with) Declarative Programs.
Proceedings of the 3rd international ACM SIGPLAN conference on Principles and practice of declarative programming, 2001

Net Reductions for LTL Model-Checking.
Proceedings of the Correct Hardware Design and Verification Methods, 2001

A BDD-Based Model Checker for Recursive Programs.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001

More Infinite Results.
Proceedings of the Current Trends in Theoretical Computer Science, 2001

2000
An efficient automata approach to some problems on context-free grammars.
Inf. Process. Lett., 2000

Verification of Safety Properties Using Integer Programming: Beyond the State Equation.
Formal Methods Syst. Des., 2000

A Uniform Framework for Problems on Context-Free Grammars.
Bull. EATCS, 2000

Efficient Algorithms for pre<sup>*</sup> and post<sup>*</sup> on Interprocedural Parallel Flow Graphs.
Proceedings of the POPL 2000, 2000

Verification of Systems with an Infinite State Space.
Proceedings of the Modeling and Verification of Parallel Processes, 4th Summer School, 2000

Verifying Single and Multi-mutator Garbage Collectors with Owicki-Gries in Isabelle/HOL.
Proceedings of the Mathematical Foundations of Computer Science 2000, 2000

A New Unfolding Approach to LTL Model Checking.
Proceedings of the Automata, Languages and Programming, 27th International Colloquium, 2000

Efficient Algorithms for Model Checking Pushdown Systems.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000

1999
Petri Nets and Regular Processes.
J. Comput. Syst. Sci., 1999

On the Verification of Broadcast Protocols.
Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

An Automata-Theoretic Approach to Interprocedural Data-Flow Analysis.
Proceedings of the Foundations of Software Science and Computation Structure, 1999

Constraint-Based Analysis of Broadcast Protocols.
Proceedings of the Computer Science Logic, 13th International Workshop, 1999

Proof-Checking Protocols Using Bisimulations.
Proceedings of the CONCUR '99: Concurrency Theory, 1999

An Unfolding Algorithm for Synchronous Products of Transition Systems.
Proceedings of the CONCUR '99: Concurrency Theory, 1999

1998
Reachability in Live and Safe Free-Choice Petri Nets is NP-Complete.
Theor. Comput. Sci., 1998

1997
Petri Nets, Commutative Context-Free Grammars, and Basic Parallel Processes.
Fundam. Informaticae, 1997

Decidability of Model Checking for Infinite-State Concurrent Systems.
Acta Informatica, 1997

Reachability Analysis of Pushdown Automata: Application to Model-Checking.
Proceedings of the CONCUR '97: Concurrency Theory, 1997

An Automata Approach to Some Problems on Context-Free Grammars.
Proceedings of the Foundations of Computer Science: Potential - Theory, 1997

Model Checking LTL Using Constraint Programming.
Proceedings of the Application and Theory of Petri Nets 1997, 1997

1996
Trapping Mutual Exclusion in the Box Calculus.
Theor. Comput. Sci., 1996

More infinite results.
Proceedings of the First International Workshop on Verification of Infinite State Systems, 1996

Deciding Finiteness of Petri Nets Up To Bisimulation.
Proceedings of the Automata, Languages and Programming, 23rd International Colloquium, 1996

An Effective Tableau System for the Linear Time µ-Calculus.
Proceedings of the Automata, Languages and Programming, 23rd International Colloquium, 1996

Checking System Properties via Integer Programming.
Proceedings of the Programming Languages and Systems, 1996

Verification Using PEP.
Proceedings of the Algebraic Methodology and Software Technology, 1996

Decidability and Complexity of Petri Net Problems - An Introduction.
Proceedings of the Lectures on Petri Nets I: Basic Models, 1996

1995
Complexity Results for 1-Safe Nets.
Theor. Comput. Sci., 1995

Shortest Paths in Reachability Graphs.
J. Comput. Syst. Sci., 1995

On the Model Checking Problem for Branching Time Logics and Basic Parallel Processes.
Proceedings of the Computer Aided Verification, 1995

1994
Reduction and Synthesis of Live and Bounded Free Choice Petri Nets
Inf. Comput., October, 1994

Model Checking Using Net Unfoldings.
Sci. Comput. Program., 1994

Decidability Issues for Petri Nets - a survey.
J. Inf. Process. Cybern., 1994

Operational Semantics for the Petri Box Calculus.
Proceedings of the CONCUR '94, 1994

On the Decidability of Model Checking for Several µ-calculi and Petri Nets.
Proceedings of the Trees in Algebra and Programming, 1994

1993
Reachability in Cyclic Extended Free-Choice Systems.
Theor. Comput. Sci., 1993

The Asynchronous Committee Meeting Problem.
Proceedings of the Graph-Theoretic Concepts in Computer Science, 1993

General Refinement and Recursion Operators for the Petri Box Calculus.
Proceedings of the STACS 93, 1993

1992
A Polynomial-Time Algorithm to Decide Liveness of Bounded Free Choice Nets.
Theor. Comput. Sci., 1992

Traps Characterize Home States in Free Choice Systems.
Theor. Comput. Sci., 1992

A Solution to the Covering Problem for 1-Bounded Conflict-Free Petri Nets Using Linear Programming.
Inf. Process. Lett., 1992

1991
Model Checking of Persistent Petri Nets.
Proceedings of the Computer Science Logic, 5th Workshop, 1991

Compositional Synthesis of Live and Bounded Free Choice Petri Nets.
Proceedings of the CONCUR '91, 1991

1990
Reachability in reversible free-choice systems
Forschungsberichte, TU Munich, 1990

Synthesis Rules for Petri Nets, and How they Lead to New Results.
Proceedings of the CONCUR '90, 1990

Top-down synthesis of live and bounded free choice nets.
Proceedings of the Advances in Petri Nets 1991, 1990

1989
On the analysis and synthesis of free choice systems.
Proceedings of the Advances in Petri Nets 1990 [10th International Conference on Applications and Theory of Petri Nets, 1989

Circuits, handles, bridges and nets.
Proceedings of the Advances in Petri Nets 1990 [10th International Conference on Applications and Theory of Petri Nets, 1989


  Loading...