2024
Round- and context-bounded control of dynamic pushdown systems.
Formal Methods Syst. Des., June, 2024
On the Satisfiability of Local First-Order Logics with Data.
Log. Methods Comput. Sci., 2024
Branch-Well-Structured Transition Systems and Extensions.
Log. Methods Comput. Sci., 2024
A Framework for Streaming Event-Log Prediction in Business Processes.
CoRR, 2024
Permutation Equivariant Deep Reinforcement Learning for Multi-Armed Bandit.
Proceedings of the 36th IEEE International Conference on Tools with Artificial Intelligence, 2024
2023
Analysis of recurrent neural networks via property-directed verification of surrogate models.
Int. J. Softw. Tools Technol. Transf., June, 2023
Analyzing Robustness of Angluin's L<sup>*</sup> Algorithm in Presence of Noise.
CoRR, 2023
2022
Bounded Reachability Problems are Decidable in FIFO Machines.
Log. Methods Comput. Sci., 2022
Analyzing Robustness of Angluin's L* Algorithm in Presence of Noise.
Proceedings of the 13th International Symposium on Games, 2022
On the Existential Fragments of Local First-Order Logics with Data.
Proceedings of the 13th International Symposium on Games, 2022
A Survey of Model Learning Techniques for Recurrent Neural Networks.
Proceedings of the A Journey from Process Algebra via Timed Automata to Model Learning, 2022
2021
Communicating finite-state machines, first-order logic, and star-free propositional dynamic logic.
J. Comput. Syst. Sci., 2021
Extracting Context-Free Grammars from Recurrent Neural Networks using Tree-Automata Learning and A* Search.
Proceedings of the 15th International Conference on Grammatical Inference, 2021
Local First-Order Logic with Two Data Values.
Proceedings of the 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2021
Reachability in Distributed Memory Automata.
Proceedings of the 29th EACSL Annual Conference on Computer Science Logic, 2021
A Unifying Framework for Deciding Synchronizability.
Proceedings of the 32nd International Conference on Concurrency Theory, 2021
Property-Directed Verification and Robustness Certification of Recurrent Neural Networks.
Proceedings of the Automated Technology for Verification and Analysis, 2021
2020
Erratum to "Frequency Linear-time Temporal Logic".
CoRR, 2020
Property-Directed Verification of Recurrent Neural Networks.
CoRR, 2020
Synthesis in Presence of Dynamic Links.
Proceedings of the Proceedings 11th International Symposium on Games, 2020
Parameterized Synthesis for Fragments of First-Order Logic Over Data Words.
Proceedings of the Foundations of Software Science and Computation Structures, 2020
2019
The Complexity of Flat Freeze LTL.
Log. Methods Comput. Sci., 2019
Non-Sequential Theory of Distributed Systems.
CoRR, 2019
Identifiers in Registers - Describing Network Algorithms with Logic.
Proceedings of the Foundations of Software Science and Computation Structures, 2019
2018
An automata-theoretic approach to the verification of distributed algorithms.
Inf. Comput., 2018
Realizability of concurrent recursive programs.
Formal Methods Syst. Des., 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
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
Round-Bounded Control of Parameterized Systems.
Proceedings of the Automated Technology for Verification and Analysis, 2018
2017
The Complexity of Model Checking Multi-Stack Systems.
Theory Comput. Syst., 2017
Emptiness of Ordered Multi-Pushdown Automata is 2ETIME-Complete.
Int. J. Found. Comput. Sci., 2017
2016
On Parameterized One-Counter Automata.
CoRR, 2016
One-Counter Automata with Counter Visibility.
CoRR, 2016
One-Counter Automata with Counter Observability.
Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2016
2015
Automata and Logics for Concurrent Systems: Five Models in Five Pages.
Proceedings of the Implementation and Application of Automata, 2015
Towards Formal Verification of Distributed Algorithms.
Proceedings of the 22nd International Symposium on Temporal Representation and Reasoning, 2015
Automata and Logics for Concurrent Systems: Realizability and Verification.
, 2015
2014
Pebble Weighted Automata and Weighted Logics.
ACM Trans. Comput. Log., 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
A Robust Class of Data Languages and an Application to Learning.
Log. Methods Comput. Sci., 2014
Parameterized Verification of Communicating Automata under Context Bounds.
Proceedings of the Reachability Problems - 8th International Workshop, 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
Logic for communicating automata with parameterized topology.
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
2013
Event clock message passing automata: a logical characterization and an emptiness checking algorithm.
Formal Methods Syst. Des., 2013
Dynamic Communicating Automata and Branching High-Level MSCs.
Proceedings of the Language and Automata Theory and Applications, 2013
Weighted Specifications over Nested Words.
Proceedings of the Foundations of Software Science and Computation Structures, 2013
A Fresh Approach to Learning Register Automata.
Proceedings of the Developments in Language Theory - 17th International Conference, 2013
2012
An optimal construction of Hanf sentences.
J. Appl. Log., 2012
Frequency Linear-time Temporal Logic.
Proceedings of the Sixth International Symposium on Theoretical Aspects of Software Engineering, 2012
Model Checking Languages of Data Words.
Proceedings of the Foundations of Software Science and Computational Structures, 2012
A Probabilistic Kleene Theorem.
Proceedings of the Automated Technology for Verification and Analysis, 2012
2011
An Automaton over Data Words That Captures EMSO Logic.
Proceedings of the CONCUR 2011 - Concurrency Theory - 22nd International Conference, 2011
2010
Learning Communicating Automata from MSCs.
IEEE Trans. Software Eng., 2010
Propositional Dynamic Logic for Message-Passing Systems
Log. Methods Comput. Sci., 2010
SMA - The Smyle Modeling Approach.
Comput. Informatics, 2010
Pebble Weighted Automata and Transitive Closure Logics.
Proceedings of the Automata, Languages and Programming, 37th International Colloquium, 2010
Realizability of Dynamic MSC Languages.
Proceedings of the Computer Science, 2010
libalf: The Automata Learning Framework.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010
2009
Angluin-Style Learning of NFA.
Proceedings of the IJCAI 2009, 2009
Weighted versus Probabilistic Logics.
Proceedings of the Developments in Language Theory, 13th International Conference, 2009
2008
On the Expressive Power of 2-Stack Visibly Pushdown Automata.
Log. Methods Comput. Sci., 2008
Muller message-passing automata and logics.
Inf. Comput., 2008
Emptiness of Multi-pushdown Automata Is 2ETIME-Complete.
Proceedings of the Developments in Language Theory, 12th International Conference, 2008
Smyle: A Tool for Synthesizing Distributed Models from Scenarios by Learning.
Proceedings of the CONCUR 2008 - Concurrency Theory, 19th International Conference, 2008
2007
Replaying Play In and Play Out: Synthesis of Design Models from Scenarios by Learning.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007
Weighted Distributed Systems and Their Logics.
Proceedings of the Logical Foundations of Computer Science, International Symposium, 2007
Automata and Logics for Timed Message Sequence Charts.
Proceedings of the FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science, 2007
2006
Message-passing automata are expressively equivalent to EMSO logic.
Theor. Comput. Sci., 2006
MSCan - A Tool for Analyzing MSC Specifications.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006
Formal Models of Communicating Systems - Languages, Automata, and Monadic Second-Order Logic
Springer, ISBN: 3-540-32922-6, 2006
2005
Automata and logics for message sequence charts.
PhD thesis, 2005
A Hierarchy of Implementable MSC Languages.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2005
On the Expressiveness of Asynchronous Cellular Automata.
Proceedings of the Fundamentals of Computation Theory, 15th International Symposium, 2005
2004
Verifying Qualitative Properties of Probabilistic Programs.
Proceedings of the Validation of Stochastic Systems - A Guide to Current Research, 2004
Controller Synthesis for Probabilistic Systems.
Proceedings of the Exploring New Frontiers of Theoretical Informatics, 2004
2003
Deciding LTL over Mazurkiewicz traces.
Data Knowl. Eng., 2003
Model Checking Probabilistic Distributed Systems.
Proceedings of the Advances in Computing Science, 2003
2002
Local Parallel Model Checking for the Alternation-Free µ-Calculus.
Proceedings of the Model Checking of Software, 2002
Extending Compositional Message Sequence Graphs.
Proceedings of the Logic for Programming, 2002
Generalised Regular MSC Languages.
Proceedings of the Foundations of Software Science and Computation Structures, 2002
2001
Modelling, Specifying, and Verifying Message Passing Systems.
Proceedings of the Eigth International Symposium on Temporal Representation and Reasoning, 2001
Parallel Model Checking for the Alternation Free µ-Calculus.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2001