4 citations · 18 across the 15 of their papers we have counts for
16 papers
First-Order LTLf Synthesis with Lookback (Extended Version)
Sarah Winkler
Reactive synthesis addresses the problem of generating a controller for a temporal specification in an adversarial environment; it was typically studied for LTL. Driven by applicat…
Decidable Fragments of LTLf Modulo Theories (Extended Version)
Luca Geatti, Alessandro Gianola, Nicola Gigante +1
We study Linear Temporal Logic Modulo Theories over Finite Traces (LTLfMT), a recently introduced extension of LTL over finite traces (LTLf) where propositions are replaced by firs…
Monitoring Arithmetic Temporal Properties on Finite Traces
Paolo Felli, Marco Montali, Fabio Patrizi +1
We study monitoring of linear-time arithmetic properties against finite traces generated by an unknown dynamic system. The monitoring state is determined by considering at once the…
Conformance Checking with Uncertainty via SMT (Extended Version)
Paolo Felli, Alessandro Gianola, Marco Montali +2
Logs of real-life processes often feature uncertainty pertaining the recorded timestamps, data values, and/or events. We consider the problem of checking conformance of uncertain l…
CTL* model checking for data-aware dynamic systems with arithmetic
Paolo Felli, Marco Montali, Sarah Winkler
The analysis of complex dynamic systems is a core research topic in formal methods and AI, and combined modelling of systems with data has gained increasing importance in applicati…
Soundness of Data-Aware Processes with Arithmetic Conditions
Paolo Felli, Marco Montali, Sarah Winkler
Data-aware processes represent and integrate structural and behavioural constraints in a single model, and are thus increasingly investigated in business process management and inf…
Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic
Paolo Felli, Marco Montali, Sarah Winkler
Combined modeling and verification of dynamic systems and the data they operate on has gained momentum in AI and in several application domains. We investigate the expressive yet c…
CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version)
Paolo Felli, Alessandro Gianola, Marco Montali +2
Conformance checking is a key process mining task for comparing the expected behavior captured in a process model and the actual behavior recorded in a log. While this problem has…
Runtime Complexity Analysis of Logically Constrained Rewriting
Sarah Winkler, Georg Moser
Logically constrained rewrite systems (LCTRSs) are a versatile and efficient rewriting formalism that can be used to model programs from various programming paradigms, as well as s…
Tools in Term Rewriting for Education
Sarah Winkler, Aart Middeldorp
Term rewriting is a Turing complete model of computation. When taught to students of computer science, key properties of computation as well as techniques to analyze programs on an…
Proceedings of the Second International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements
Martin Suda, Sarah Winkler
These are the post-proceedings of the second ARCADE workshop, which took place on the 26th August 2019 in Natal, Brazil, colocated with CADE-27. ARCADE stands for Automated Reasoni…
Smarter Features, Simpler Learning?
Sarah Winkler, Georg Moser
Earlier work on machine learning for automated reasoning mostly relied on simple, syntactic features combined with sophisticated learning techniques. Using ideas adopted in the sof…
Certified Ordered Completion
Christian Sternagel, Sarah Winkler
On the one hand, ordered completion is a fundamental technique in equational theorem proving that is employed by automated tools. On the other hand, their complexity makes such too…
Abstract Completion, Formalized
Nao Hirokawa, Aart Middeldorp, Christian Sternagel +1
Completion is one of the most studied techniques in term rewriting and fundamental to automated reasoning with equalities. In this paper we present new correctness proofs of abstra…
AC-KBO Revisited
Akihisa Yamada, Sarah Winkler, Nao Hirokawa +1
Equational theories that contain axioms expressing associativity and commutativity (AC) of certain operators are ubiquitous. Theorem proving methods in such theories rely on well-f…
CeTA - A Tool for Certified Termination Analysis
Christian Sternagel, René Thiemann, Sarah Winkler +1
Since the first termination competition in 2004 it is of great interest, whether a proof that has been automatically generated by a termination tool, is indeed correct. The increas…