2025
High-Level Message Sequence Charts: Satisfiability and Realizability Revisited.
Proceedings of the Application and Theory of Petri Nets and Concurrency, 2025
2024
Simulations for Event-Clock Automata.
Log. Methods Comput. Sci., 2024
Propositional dynamic logic and asynchronous cascade decompositions for regular trace languages.
CoRR, 2024
An expressively complete local past propositional dynamic logic over Mazurkiewicz traces and its applications.
Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, 2024
Reversible Transducers over Infinite Words.
Proceedings of the 35th International Conference on Concurrency Theory, 2024
MITL Model Checking via Generalized Timed Automata and a New Liveness Algorithm.
Proceedings of the 35th International Conference on Concurrency Theory, 2024
2023
A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation.
Proceedings of the Computer Aided Verification - 35th International Conference, 2023
2022
Asynchronous wreath product and cascade decompositions for concurrent behaviours.
Log. Methods Comput. Sci., 2022
Regular transducer expressions for regular transformations.
Inf. Comput., 2022
Efficient Construction of Reversible Transducers from Regular Transducer Expressions.
Proceedings of the LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2, 2022
Zone-Based Verification of Timed Automata: Extrapolations, Simulations and What Next?
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2022
CONCUR Test-Of-Time Award 2022 (Invited Paper).
Proceedings of the 33rd International Conference on Concurrency Theory, 2022
Propositional Dynamic Logic and Asynchronous Cascade Decompositions for Regular Trace Languages.
Proceedings of the 33rd International Conference on Concurrency Theory, 2022
2021
Communicating finite-state machines, first-order logic, and star-free propositional dynamic logic.
J. Comput. Syst. Sci., 2021
Reversible Regular Languages: Logical and Algebraic Characterisations.
Fundam. Informaticae, 2021
SD-Regular Transducer Expressions for Aperiodic Transformations.
Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 2021
Fast Zone-Based Algorithms for Reachability in Pushdown Timed Automata.
Proceedings of the Computer Aided Verification - 33rd International Conference, 2021
2020
Wreath/cascade products and related decomposition results for the concurrent setting of Mazurkiewicz traces (extended version).
CoRR, 2020
Revisiting Underapproximate Reachability for Multipushdown Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020
Register Transducers Are Marble Transducers.
Proceedings of the 45th International Symposium on Mathematical Foundations of Computer Science, 2020
Reachability for Updatable Timed Automata Made Faster and More Effective.
Proceedings of the 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2020
Weighted Tiling Systems for Graphs: Evaluation Complexity.
Proceedings of the 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2020
Wreath/Cascade Products and Related Decomposition Results for the Concurrent Setting of Mazurkiewicz Traces.
Proceedings of the 31st International Conference on Concurrency Theory, 2020
2019
Non-Sequential Theory of Distributed Systems.
CoRR, 2019
Aperiodic Weighted Automata and Weighted First-Order Logic.
Proceedings of the 44th International Symposium on Mathematical Foundations of Computer Science, 2019
Timed Systems through the Lens of Logic.
Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, 2019
Logics for Reversible Regular Languages and Semigroups with Involution.
Proceedings of the Developments in Language Theory - 23rd International Conference, 2019
Fast Algorithms for Handling Diagonal Constraints in Timed Automata.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019
Modular Descriptions of Regular Functions.
Proceedings of the Algebraic Informatics - 8th International Conference, 2019
2018
A unifying survey on weighted logics and weighted automata - Core weighted logic: minimal and versatile specification of quantitative properties.
Soft Comput., 2018
Analyzing Timed Systems Using Tree Automata.
Log. Methods Comput. Sci., 2018
An automata-theoretic approach to the verification of distributed algorithms.
Inf. Comput., 2018
Unambiguous Forest Factorization.
CoRR, 2018
Gossiping in Message-Passing Systems.
CoRR, 2018
Communicating Finite-State Machines and Two-Variable Logic.
Proceedings of the 35th Symposium on Theoretical Aspects of Computer Science, 2018
Reachability in Timed Automata with Diagonal Constraints.
Proceedings of the 29th International Conference on Concurrency Theory, 2018
It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with "Happened Before".
Proceedings of the 29th International Conference on Concurrency Theory, 2018
2017
Towards an Efficient Tree Automata Based Technique for Timed Systems.
Proceedings of the 28th International Conference on Concurrency Theory, 2017
2016
Nested Words for Order-2 Pushdown Systems.
CoRR, 2016
Verification of Parameterized Communicating Automata via Split-Width.
Proceedings of the Foundations of Software Science and Computation Structures, 2016
2015
Checking conformance for time-constrained scenario-based specifications.
Theor. Comput. Sci., 2015
2014
Pebble Weighted Automata and Weighted Logics.
ACM Trans. Comput. Log., 2014
Adding pebbles to weighted automata: Easy specification & efficient evaluation.
Theor. Comput. Sci., 2014
Temporal logics for concurrent recursive programs: Satisfiability and model checking.
J. Appl. Log., 2014
Distributed Timed Automata with Independently Evolving Clocks.
Fundam. Informaticae, 2014
Parameterized Verification of Communicating Automata under Context Bounds.
Proceedings of the Reachability Problems - 8th International Workshop, 2014
Reasoning About Distributed Systems: WYSIWYG (Invited Talk).
Proceedings of the 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, 2014
Parameterized Communicating Automata: Complementation and Model Checking.
Proceedings of the 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, 2014
Logical characterization of weighted pebble walking automata.
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014
Controllers for the Verification of Communicating Multi-pushdown Systems.
Proceedings of the CONCUR 2014 - Concurrency Theory - 25th International Conference, 2014
Verifying Communicating Multi-pushdown Systems via Split-Width.
Proceedings of the Automated Technology for Verification and Analysis, 2014
2013
Fair Synthesis for Asynchronous Distributed Systems.
ACM Trans. Comput. Log., 2013
Event clock message passing automata: a logical characterization and an emptiness checking algorithm.
Formal Methods Syst. Des., 2013
Weighted Specifications over Nested Words.
Proceedings of the Foundations of Software Science and Computation Structures, 2013
2012
Decidability of well-connectedness for distributed synthesis.
Inf. Process. Lett., 2012
Adding Pebbles to Weighted Automata.
Proceedings of the Implementation and Application of Automata, 2012
Model Checking Languages of Data Words.
Proceedings of the Foundations of Software Science and Computational Structures, 2012
MSO Decidability of Multi-Pushdown Systems via Split-Width.
Proceedings of the CONCUR 2012 - Concurrency Theory - 23rd International Conference, 2012
A Probabilistic Kleene Theorem.
Proceedings of the Automated Technology for Verification and Analysis, 2012
Specification and Verification using Temporal Logics.
Proceedings of the Modern Applications of Automata Theory., 2012
2010
Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces.
Inf. Comput., 2010
Pebble Weighted Automata and Transitive Closure Logics.
Proceedings of the Automata, Languages and Programming, 37th International Colloquium, 2010
Model checking time-constrained scenario-based specifications.
Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2010
10031 Executive Summary - Quantitative Models: Expressiveness and Analysis.
Proceedings of the Quantitative Models: Expressiveness and Analysis, 17.01. - 22.01.2010, 2010
10031 Abstracts Collection - Quantitative Models: Expressiveness and Analysis.
Proceedings of the Quantitative Models: Expressiveness and Analysis, 17.01. - 22.01.2010, 2010
2009
Distributed synthesis for well-connected architectures.
Formal Methods Syst. Des., 2009
Natural Specifications Yield Decidability for Distributed Synthesis of Asynchronous Systems.
Proceedings of the SOFSEM 2009: Theory and Practice of Computer Science, 2009
Weighted versus Probabilistic Logics.
Proceedings of the Developments in Language Theory, 13th International Conference, 2009
2008
On Aperiodic and Star-Free Formal Power Series in Partially Commuting Variables.
Theory Comput. Syst., 2008
A Survey on Small Fragments of First-Order Logic over Finite Words.
Int. J. Found. Comput. Sci., 2008
First-order definable languages.
Proceedings of the Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas]., 2008
2007
Weighted automata and weighted logics.
Theor. Comput. Sci., 2007
Uniform Satisfiability in PSPACE for Local Temporal Logics Over Mazurkiewicz Traces.
Fundam. Informaticae, 2007
Timed substitutions for regular signal-event languages.
Formal Methods Syst. Des., 2007
Minimal Counterexample Generation for SPIN.
Proceedings of the Model Checking Software, 2007
Automata and Logics for Timed Message Sequence Charts.
Proceedings of the FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science, 2007
Local Testing of Message Sequence Charts Is Difficult.
Proceedings of the Fundamentals of Computation Theory, 16th International Symposium, 2007
2006
From local to global temporal logics over Mazurkiewicz traces.
Theor. Comput. Sci., 2006
J. Autom. Lang. Comb., 2006
Pure future local temporal logics are expressively complete for Mazurkiewicz traces.
Inf. Comput., 2006
Refinements and Abstractions of Signal-Event (Timed) Languages.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2006
Intersection of Regular Signal-Event (Timed) Languages.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2006
A Fresh Look at Testing for Asynchronous Communication.
Proceedings of the Automated Technology for Verification and Analysis, 2006
2004
A simple process algebra based on atomic actions with resources.
Math. Struct. Comput. Sci., 2004
Local temporal logic is expressively complete for cograph dependence alphabets.
Inf. Comput., 2004
Minimization of Counterexamples in SPIN.
Proceedings of the Model Checking Software, 2004
Distributed Games and Distributed Control for Asynchronous Systems.
Proceedings of the LATIN 2004: Theoretical Informatics, 2004
Distributed Games with Causal Memory Are Decidable for Series-Parallel Systems.
Proceedings of the FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 2004
2003
LTL with Past and Two-Way Very-Weak Alternating Automata.
Proceedings of the Mathematical Foundations of Computer Science 2003, 2003
Local LTL with Past Constants Is Expressively Complete for Mazurkiewicz Traces.
Proceedings of the Mathematical Foundations of Computer Science 2003, 2003
Satisfiability and Model Checking for MSO-definable Temporal Logics are in PSPACE.
Proceedings of the CONCUR 2003, 2003
2002
Resource traces: a domain for processes sharing exclusive resources.
Theor. Comput. Sci., 2002
A truly concurrent semantics for a process algebra using resource pomsets.
Theor. Comput. Sci., 2002
LTL Is Expressively Complete for Mazurkiewicz Traces.
J. Comput. Syst. Sci., 2002
J. Autom. Lang. Comb., 2002
An Elementary Expressively Complete Temporal Logic for Mazurkiewicz Traces.
Proceedings of the Automata, Languages and Programming, 29th International Colloquium, 2002
Safety and Liveness Properties for Real Traces and a Direct Translation from LTL to Monoids.
Proceedings of the Formal and Natural Computing, 2002
2001
Model Checking Systems of Replicated Processes with Spin.
Proceedings of the Model Checking Software, 2001
Avoiding State Explosion for Distributed Systems with Timestamps.
Proceedings of the FME 2001: Formal Methods for Increasing Software Productivity, 2001
Fast LTL to Büchi Automata Translation.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001
2000
Asynchronous cellular automata for pomsets.
Theor. Comput. Sci., 2000
1999
The Kleene-Schützenberger Theorem for Formal Power Series in Partially Commuting Variables.
Inf. Comput., 1999
A Truly Concurrent Semantics for a Simple Parallel Programming Language.
Proceedings of the Computer Science Logic, 13th International Workshop, 1999
An Expressively Complete Temporal Logic without Past Tense Operators for Mazurkiewicz Traces.
Proceedings of the Computer Science Logic, 13th International Workshop, 1999
1998
Characterization of the Expressive Power of Silent Transitions in Timed Automata.
Fundam. Informaticae, 1998
A (Non-elementary) Modular Decision Procedure for LTrL.
Proceedings of the Mathematical Foundations of Computer Science 1998, 1998
1997
Removing epsilon-Transitions in Timed Automata.
Proceedings of the STACS 97, 14th Annual Symposium on Theoretical Aspects of Computer Science, Lübeck, Germany, February 27, 1997
On Recognizable and Rational Formal Power Series in Partially Commuting Variables.
Proceedings of the Automata, Languages and Programming, 24th International Colloquium, 1997
1996
On the Power of Non-Observable Actions in Timed Automata.
Proceedings of the STACS 96, 1996
Asynchronous Cellular Automata for Pomsets Without Auto-concurrency.
Proceedings of the CONCUR '96, 1996
1995
Rational and Recognizable Complex Trace Languages
Inf. Comput., January, 1995
On Congruences and Partial Orders.
Proceedings of the Mathematical Foundations of Computer Science 1995, 1995
A Domain for Concurrent Termination: A Generalization of Mazurkiewicz Traces (Extended Abstract).
Proceedings of the Automata, Languages and Programming, 22nd International Colloquium, 1995
Recent Developments in Trace Theory.
Proceedings of the Developments in Language Theory II, 1995
Proceedings of the Book of Traces, 1995
1994
An Extension of Kleene's and Ochmanski's Theorems to Infinite Traces.
Theor. Comput. Sci., 1994
1993
The Poset of Infinitary Traces.
Theor. Comput. Sci., 1993
An Efficient Crash-tolerant Sequential Traversal.
Parallel Process. Lett., 1993
1992
Decidability of the Star Problem in A* x {b}*.
Inf. Process. Lett., 1992
Poset Properties of Complex Traces.
Proceedings of the Mathematical Foundations of Computer Science 1992, 1992
Asynchronous Cellular Automata for Infinite Traces.
Proceedings of the Automata, Languages and Programming, 19th International Colloquium, 1992
A survey of recognizable languages with infinite traces.
Proceedings of the Advances in Petri Nets 1992, The DEMON Project, 1992
1991
Recognizable and Rational Languages of Finite and Infinite Traces.
Proceedings of the STACS 91, 1991
Recognizable Complex Trace Languages.
Proceedings of the Mathematical Foundations of Computer Science 1991, 1991
A Kleene Theorem for Infinite Trace Languages.
Proceedings of the Automata, Languages and Programming, 18th International Colloquium, 1991
1990
Un Modèle Asynchrone pour les Systèmes Distribués.
Theor. Comput. Sci., 1990
A Linear Fault-Tolerant Naming Algorithm.
Proceedings of the Distributed Algorithms, 4th International Workshop, 1990
Proceedings of the Semantics of Systems of Concurrent Processes, 1990