6 citations
Counting papers with at most 25 authors, so collaboration author lists do not stand in for the people here.
- Centre National de la Recherche ScientifiqueFR9 papers
- Institut de Recherche en Informatique FondamentaleFR3 papers
- Université Paris CitéFR3 papers
- Université Paris-SaclayFR3 papers
- Aalborg UniversityDK2 papers
- Czech Academy of Sciences, Institute of SociologyCZ2 papers
- Herzliya Medical CenterIL2 papers
- Laboratoire Méthodes FormellesFR2 papers
- Masaryk UniversityCZ2 papers
- Paris-Est SupFR2 papers
- Radboud University NijmegenNL2 papers
- Sorbonne Paris CitéFR2 papers
32 papers · 1 filter
Asynchronous Composition of LTL Properties over Infinite and Finite Traces
Alberto Bombardelli, Stefano Tonetta
The verification of asynchronous software components poses significant challenges due to the way components interleave and exchange input/output data concurrently. Compositional st…
Completions of Kleene's second model
Sebastiaan A. Terwijn
We investigate completions of partial combinatory algebras (pcas), in particular of Kleene's second model and generalizations thereof. We consider weak and strong n…
Moving a Derivation Along a Derivation Preserves the Spine in Adhesive Categories
Hans-Jörg Kreowski, Aaron Lye, Aljoscha Windhorst
In this paper, we investigate the relationship between two elementary operations on derivations in the framework of graph transformation based on adhesive categories: moving a deri…
What Monads Can and Cannot Do with a Few Extra Pages
Rasmus Ejlers Møgelberg, Maaike Zwart
The delay monad provides a way to introduce general recursion in type theory. To write programs that use a wide range of computational effects directly in type theory, we need to c…
Multi-representation associated to the numbering of a subbasis and formal inclusion relations
Emmanuel Rauzy
We revisit Dieter Spreen's notion of a representation associated to a numbered basis equipped with a strong inclusion relation. We show that by relaxing his requirements, we obtain…
The Complexity of Second-order HyperLTL
Hadar Frenkel, Gaëtan Regaud, Martin Zimmermann
We determine the complexity of second-order HyperLTL satisfiability, finite-state satisfiability, and model-checking: All three are equivalent to truth in third-order arithmetic. W…
Crash-Stop Failures in Asynchronous Multiparty Session Types
Adam D. Barwell, Ping Hou, Nobuko Yoshida +1
Session types provide a typing discipline for message-passing systems. However, their theory often assumes an ideal world: one in which everything is reliable and without failures.…
A higher-order transformation approach to the formalization and analysis of BPMN using graph transformation systems
Tim Kräuter, Adrian Rutle, Harald König +1
The Business Process Modeling Notation (BPMN) is a widely used standard notation for defining intra- and inter-organizational workflows. However, the informal description of the BP…
Enumeration and updates for conjunctive linear algebra queries through expressibility
Thomas Muñoz, Cristian Riveros, Stijn Vansummeren
Due to the importance of linear algebra and matrix operations in data analytics, there is significant interest in using relational query optimization and processing techniques for…
An axiomatization for the universal theory of the Heisenberg group
Anthony M. Gaglione, Dennis Spellman
The Heisenberg group, here denoted , is the group of all upper unitriangular matrices with entries in the ring of integers. A.G. Myasnikov posed the que…
Offline and Online Use of Interval and Set-Based Approaches for Control and State Estimation: A Selection of Methodological Approaches and Their Application
Andreas Rauh, Marit Lahme, Simon Rohou +4
Control and state estimation procedures need to be robust against imprecisely known parameters, uncertainty in initial conditions, and external disturbances. Interval methods and o…
Feasability of Learning Weighted Automata on a Semiring
Laure Daviaud, Marianne Johnson
Since the seminal work by Angluin and the introduction of the L*-algorithm, active learning of automata by membership and equivalence queries has been extensively studied to learn…
FMplex: Exploring a Bridge between Fourier-Motzkin and Simplex
Valentin Promies, Jasper Nalbach, Erika Ábrahám +1
In this paper we present a quantifier elimination method for conjunctions of linear real arithmetic constraints. Our algorithm is based on the Fourier-Motzkin variable elimination…
Worst-Case Input Generation for Concurrent Programs under Non-Monotone Resource Metrics
Long Pham, Jan Hoffmann
Worst-case input generation aims to automatically generate inputs that exhibit the worst-case performance of programs. It has several applications, and can, for example, detect vul…
Sharing proofs with predicative theories through universe-polymorphic elaboration
Thiago Felicissimo, Frédéric Blanqui
As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the…
The Expansion Problem for Infinite Trees
Achim Blumensath
We study Ramsey like theorems for infinite trees and similar combinatorial tools. As an application we consider the expansion problem for tree algebras.
Rewriting and Completeness of Sum-Over-Paths in Dyadic Fragments of Quantum Computing
Renaud Vilmart
The "Sum-Over-Paths" formalism is a way to symbolically manipulate linear maps that describe quantum systems, and is a tool that is used in formal verification of such systems. We…
Hydra Battles and AC Termination
Nao Hirokawa, Aart Middeldorp
We present a new encoding of the Battle of Hercules and Hydra as a rewrite system with AC symbols. Unlike earlier term rewriting encodings, it faithfully models any strategy of Her…
Discounted-Sum Automata with Multiple Discount Factors
Udi Boker, Guy Hefetz
Discounting the influence of future events is a key paradigm in economics and it is widely used in computer-science models, such as games, Markov decision processes (MDPs), reinfor…
Termination of Graph Transformation Systems via Generalized Weighted Type Graphs
Jörg Endrullis, Roy Overbeek
We refine the weighted type graph technique for proving termination of double pushout (DPO) graph transformation systems. We increase the power of the approach for graphs, we gener…
Safety and Liveness of Quantitative Properties and Automata
Udi Boker, Thomas A. Henzinger, Nicolas Mazzocchi +1
Safety and liveness stand as fundamental concepts in formal languages, playing a key role in verification. The safety-liveness classification of boolean properties characterizes wh…
Exploiting Uncertainty for Querying Inconsistent Description Logics Knowledge Bases
Riccardo Zese, Evelina Lamma, Fabrizio Riguzzi
The necessity to manage inconsistency in Description Logics Knowledge Bases (KBs) has come to the fore with the increasing importance gained by the Semantic Web, where information…
Analyzing Robustness of Angluin's L Algorithm in Presence of Noise
Lina Ye, Igor Khmelnitsky, Serge Haddad +5
Angluin's L algorithm learns the minimal deterministic finite automaton (DFA) of a regular language using membership and equivalence queries. Its probabilistic approximatively…
Fractals from Regular Behaviours
Todd Schmid, Victoria Noquez, Lawrence S. Moss
We forge connections between the theory of fractal sets obtained as attractors of iterated function systems and process calculi. To this end, we reinterpret Milner's expressions fo…