(𝑚⋅log𝑛) where n" role="presentation">𝑛 and m" role="presentation">𝑚 are the numbers of nodes and edges, respectively. The generic complexity result and the possibility of combining system types yields a toolbox for efficient partition refinement algorithms. Instances of our generic algorithm match the run-time of the best known algorithms for unlabelled transition systems, Markov chains, deterministic automata (with fixed alphabets), Segala systems, and for color refinement.}, author = {Wißmann, Thorsten and Dorsch, Ulrich and Milius, Stefan and Schröder, Lutz}, faupublication = {yes}, journal = {Logical Methods in Computer Science}, pages = {1–63}, peerreviewed = {Yes}, title = {{Efficient} and {Modular} {Coalgebraic} {Partition} {Refinement}}, volume = {16}, year = {2020} } @inproceedings{faucris.106397764, author = {Dorsch, Ulrich and Milius, Stefan and Schröder, Lutz and Wißmann, Thorsten}, booktitle = {Proc. 28th International Conference on Concurrency Theory (CONCUR 2017)}, editor = {Meyer R, Nestmann U}, faupublication = {yes}, pages = {28:1--28:16}, peerreviewed = {Yes}, publisher = {Schloss Dagstuhl}, title = {{Efficient} {Coalgebraic} {Partition} {Refinement}}, volume = {85}, year = {2017} } @inproceedings{faucris.264571269, abstract = {We provide a generic algorithm for constructing formulae that distinguish behaviourally inequivalent states in systems of various transition types such as nondeterministic, probabilistic or weighted; genericity over the transition type is achieved by working with coalgebras for a set functor in the paradigm of universal coalgebra. For every behavioural equivalence class in a given system, we construct a formula which holds precisely at the states in that class. The algorithm instantiates to deterministic finite automata, transition systems, labelled Markov chains, and systems of many other types. The ambient logic is a modal logic featuring modalities that are generically extracted from the functor; these modalities can be systematically translated into custom sets of modalities in a postprocessing step. The new algorithm builds on an existing coalgebraic partition refinement algorithm. It runs in time O((m + n) log n) on systems with n states and m transitions, and the same asymptotic bound applies to the dag size of the formulae it constructs. This improves the bounds on run time and formula size compared to previous algorithms even for previously known specific instances, viz. transition systems and Markov chains; in particular, the best previous bound for transition systems was O(mn).}, author = {Wißmann, Thorsten and Milius, Stefan and Schröder, Lutz}, booktitle = {Leibniz International Proceedings in Informatics, LIPIcs}, date = {2021-08-24/2021-08-27}, doi = {10.4230/LIPIcs.CONCUR.2021.32}, editor = {Serge Haddad, Daniele Varacca}, faupublication = {yes}, isbn = {9783959772037}, keywords = {Bisimulation; Coalgebra; Distinguishing formulae; Modal logic; Partition refinement}, note = {CRIS-Team Scopus Importer:2021-10-01}, peerreviewed = {unknown}, publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing}, title = {{Explaining} {Behavioural} {Inequivalence} {Generically} in {Quasilinear} {Time}}, venue = {Virtual, Online}, volume = {203}, year = {2021} } @inproceedings{faucris.242406255, abstract = {Behavioural equivalences can be characterized via bisimulation, modal logics, and spoiler-duplicator games. In this paper we work in the general setting of coalgebra and focus on generic algorithms for computing the winning strategies of both players in a bisimulation game. The winning strategy of the spoiler (if it exists) is then transformed into a modal formula that distinguishes the given non-bisimilar states. The modalities required for the formula are also synthesized on-the-fly, and we present a recipe for re-coding the formula with different modalities, given by a separating set of predicate liftings. Both the game and the generation of the distinguishing formulas have been implemented in a tool called T-Beg.}, author = {König, Barbara and Mika-Michalski, Christina and Schröder, Lutz}, booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)}, date = {2020-04-25/2020-04-26}, doi = {10.1007/978-3-030-57201-3{\_}8}, editor = {Daniela Petrisan, Jurriaan Rot}, faupublication = {yes}, isbn = {9783030572006}, keywords = {Bisimulation games; Coalgebra; Distinguishing formulas; Generic partition refinement}, note = {CRIS-Team Scopus Importer:2020-09-11}, pages = {133-154}, peerreviewed = {unknown}, publisher = {Springer}, title = {{Explaining} non-bisimilarity in a coalgebraic approach: {Games} and distinguishing formulas}, venue = {Dublin}, volume = {12094 LNCS}, year = {2020} } @article{faucris.113621904, abstract = {We study a composition operation on monads, equivalently presented as large equational theories. Specifically, we discuss the existence of tensors, which are combinations of theories that impose mutual commutation of the operations from the component theories. As such, they extend the sum of two theories, which is just their unrestrained combination. Tensors of theories arise in several contexts; in particular, in the semantics of programming languages, the monad transformer for global state is given by a tensor. We present two main results: we show that the tensor of two monads need not in general exist by presenting two counterexamples, one of them involving finite powerset (i.e. the theory of join semilattices); this solves a somewhat long-standing open problem, and contrasts with recent results that had ruled out previously expected counterexamples. On the other hand, we show that tensors with bounded powerset monads do exist from countable powerset upwards. © N. Bowler, S. Goncharov, P. B. Levy, and L. Schröder.}, author = {Bowler, Nathan and Goncharov, Sergey and Levy, Paul and Schröder, Lutz}, doi = {10.2168/LMCS-9(3:22)2013}, faupublication = {yes}, journal = {Logical Methods in Computer Science}, keywords = {Monads; Non-determinism; Side effects; Tensor products}, note = {UnivIS-Import:2015-03-09:Pub.2013.tech.IMMD.profes{\_}1.explor}, pages = {1-18}, peerreviewed = {Yes}, title = {{Exploring} the {Boundaries} of {Monad} {Tensorability} on {Set}}, volume = {9}, year = {2013} } @inproceedings{faucris.320046640, abstract = {We address the task of deriving fixpoint equations from modal logics characterizing behavioural equivalences and metrics (summarized under the term conformances). We rely on an earlier work that obtains Hennessy-Milner theorems as corollaries to a fixpoint preservation property along Galois connections between suitable lattices. We instantiate this to the setting of coalgebras, in which we spell out the compatibility property ensuring that we can derive a behaviour function whose greatest fixpoint coincides with the logical conformance. We then concentrate on the linear-time case, for which we study coalgebras based on the machine functor living in Eilenberg-Moore categories, a scenario for which we obtain a particularly simple logic and fixpoint equation. The theory is instantiated to concrete examples, both in the branching-time case (bisimilarity and behavioural metrics) and in the linear-time case (trace equivalences and trace distances).}, author = {Beohar, Harsh and Gurke, Sebastian and König, Barbara and Messing, Karla and Forster, Jonas and Schröder, Lutz and Wild, Paul}, booktitle = {Leibniz International Proceedings in Informatics, LIPIcs}, date = {2024-03-12/2024-03-14}, doi = {10.4230/LIPIcs.STACS.2024.10}, editor = {Olaf Beyersdorff, Mamadou Moustapha Kante, Orna Kupferman, Daniel Lokshtanov}, faupublication = {yes}, isbn = {9783959773119}, keywords = {behavioural equivalences; behavioural metrics; coalgebras; Eilenberg-Moore categories; linear-time semantics; modal logics}, note = {CRIS-Team Scopus Importer:2024-03-22}, peerreviewed = {unknown}, publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing}, title = {{Expressive} {Quantale}-{Valued} {Logics} for {Coalgebras}: {An} {Adjunction}-{Based} {Approach}}, venue = {Clermont-Ferrand, FRA}, volume = {289}, year = {2024} } @inproceedings{faucris.118582024, address = {London}, author = {Gorin, Daniel and Schröder, Lutz}, booktitle = {Advances in Modal Logic}, faupublication = {yes}, isbn = {9781848900684}, note = {UnivIS-Import:2015-04-16:Pub.2012.tech.IMMD.profes{\_}1.extend}, pages = {300-316}, peerreviewed = {Yes}, publisher = {College Publications}, series = {Advances in Modal Logic}, title = {{Extending} {ALCQ} {With} {Bounded} {Self}-{Reference}}, venue = {Kopenhagen}, volume = {9}, year = {2012} } @article{faucris.270005679, abstract = {Finitary monads on Pos are characterized as precisely the free-algebra monads of varieties of algebras. These are classes of ordered algebras specified by inequations in context. Analogously, finitary enriched monads on Pos are characterized: here we work with varieties of coherent algebras which means that their operations are monoton}, author = {Ford, Matthew and Adámek, Jiří and Milius, Stefan and Schröder, Lutz}, doi = {10.1017/S0960129521000360}, faupublication = {yes}, journal = {Mathematical Structures in Computer Science}, keywords = {posets; monad; algebraic theory}, pages = {1--23}, peerreviewed = {Yes}, title = {{Finitary} monads on the category of posets}, url = {https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/finitary-monads-on-the-category-of-posets/C4F502C0D4264D68484EE6CCB5E3590F}, year = {2021} } @inproceedings{faucris.111548624, author = {Kohlhase, Michael and Schröder, Lutz and et al.}, author_hint = {Kohlhase M., Lemburg J., Schröder L., Schulz E.}, booktitle = {2nd World Congress on Formal Methods, FM 2009}, doi = {10.1007/978-3-642-05089-3{\_}15}, faupublication = {yes}, isbn = {9783642050886}, pages = {223-238}, peerreviewed = {Yes}, support_note = {Author relations incomplete. You may find additional data in field 'author{\_}hint'}, title = {{Formal} management of {CAD}/{CAM} processes}, venue = {Eindhoven}, year = {2009} } @inproceedings{faucris.302112633, abstract = {We study the problem of digital forensic event reconstruction, i.e., the question of whether a certain event has happened in the past of an execution by a given digital system. Instead of devising new search algorithms to solve the problem directly, we defne two novel concepts in standard linear- time temporal logic and use these concepts to solve event reconstruction using established tools for model checking. The fiirst concept is that of sufficient evidence, i.e., a characterization of states whose observation is sufficient to prove that a certain event happened in the past. The second concept is that of necessary evidence, i.e., a characterization of states whose negation can be used to refute the claim that a certain event happened in the past. Using the model checker NuSMV, we built a prototype that can calculate these two sets for a given digital system in order to solve the forensic event reconstruction problem. We relate these concepts to previous work in formal event reconstruction and apply it to Gladyshev's "ACME Manufacturing" benchmark example to illustrate the usefulness of our approach and the improved notion of digital evidence.

}, author = {Gruber, Jan and Humml, Merlin and Schröder, Lutz and Freiling, Felix}, booktitle = {Proceedings of the Digital Forensics Research Conference Europe (DFRWS EU)}, date = {2023-03-21/2023-03-24}, editor = {Edita Bajramovic and Ricardo J. Rodríguez}, faupublication = {yes}, keywords = {digital evidence; digital investigations; forensic event reconstruction; formal methods; forensic computing;}, pages = {1-11}, peerreviewed = {Yes}, title = {{Formal} {Verification} of {Necessary} and {Sufficient} {Evidence} in {Forensic} {Event} {Reconstruction}}, url = {https://dfrws.org/wp-content/uploads/2023/03/2023-03-20{\_}formal-verification-of-ne-se{\_}gruber{\_}dfrws-proc.pdf}, venue = {Bonn}, year = {2023} } @article{faucris.253782820, abstract = {Partition refinement is a method for minimizing automata and transition systems of various types. Recently, we have developed a partition refinement algorithm that is generic in the transition type of the given system and matches the run time of the best known algorithms for many concrete types of systems, e.g. deterministic automata as well as ordinary, weighted, and probabilistic (labelled) transition systems. Genericity is achieved by modelling transition types as functors on sets, and systems as coalgebras. In the present work, we refine the run time analysis of our algorithm to cover additional instances, notably weighted automata and, more generally, weighted tree automata. For weights in a cancellative monoid we match, and for non-cancellative monoids such as (the additive monoid of) the tropical semiring even substantially improve, the asymptotic run time of the best known algorithms. We have implemented our algorithm in a generic tool that is easily instantiated to concrete system types by implementing a simple refinement interface. Moreover, the algorithm and the tool are modular, and partition refiners for new types of systems are obtained easily by composing pre-implemented basic functors. Experiments show that even for complex system types, the tool is able to handle systems with millions of transitions.}, author = {Wißmann, Thorsten and Deifel, Hans-Peter and Milius, Stefan and Schröder, Lutz}, doi = {10.1007/s00165-020-00526-z}, faupublication = {yes}, journal = {Formal Aspects of Computing}, note = {Created from Fastlane, WoS look-up}, peerreviewed = {Yes}, title = {{From} generic partition refinement to weighted tree automata minimization}, year = {2021} } @article{faucris.123887104, author = {Pattinson, Dirk and Schröder, Lutz}, doi = {10.1016/j.jcss.2015.02.004}, faupublication = {yes}, journal = {Journal of Computer and System Sciences}, pages = {797--798}, peerreviewed = {Yes}, title = {{From} the {Editors}}, volume = {81}, year = {2015} } @inproceedings{faucris.226669311, abstract = {The coalgebraic µ-calculus is a generic framework for fixpoint logics with varying branching types that subsumes, besides the standard relational µ-calculus, such diverse logics as the graded µ-calculus, the monotone µ-calculus, the probabilistic µ-calculus, and the alternating-time µ-calculus. In the present work, we give a local model checking algorithm for the coalgebraic µ-calculus using a coalgebraic variant of parity games that runs, under mild assumptions on the complexity of the so-called one-step satisfaction problem, in time p

inducing various notions of process equivalence, ranging from

linear-time semantics such as trace equivalence to branching-time

semantics such as strong bisimilarity. Many of these generalize to

system types beyond standard transition systems, featuring, for

example, weighted, probabilistic, or game-based transitions; this

motivates the search for suitable coalgebraic abstractions of

process equivalence that cover these orthogonal dimensions of

generality, i.e.~are generic both in the system type and in the

notion of system equivalence. In recent joint work with Kurz, we

have proposed a parametrization of system equivalence over an

embedding of the coalgebraic type functor into a monad. In the

present paper, we refine this abstraction to use graded

monads, which come with a notion of depth that corresponds, e.g.,

to trace length or bisimulation depth. We introduce a notion of

graded algebras and show how they play the role of formulas in trace

logics.

}, address = {Dagstuhl}, author = {Milius, Stefan and Pattinson, Dirk and Schröder, Lutz}, booktitle = {6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015}, date = {2015-06-24/2015-06-26}, doi = {10.4230/LIPIcs.CALCO.2015.253}, faupublication = {yes}, keywords = {Graded monad; traces; concurrent systems; bisimilarity; graded algebra; trace logic;}, pages = {253--269}, peerreviewed = {Yes}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Generic} {Trace} {Semantics} and {Graded} {Monads}}, venue = {Nijmegen}, year = {2015} } @inproceedings{faucris.203707903, address = {Dagstuhl}, author = {Hausmann, Daniel and Schröder, Lutz and Egger, Christoph}, booktitle = {Proceedings of the 27th International Conference on Concurrency Theory, CONCUR 2016}, doi = {10.4230/LIPIcs.CONCUR.2016.34}, faupublication = {yes}, keywords = {Coalgebraic logic, mu-calculus, global caching, satisfiability checking}, note = {UnivIS-Import:2018-09-06:Pub.2016.tech.IMMD.profes{\_}1.global}, pages = {34:1-34:15}, peerreviewed = {Yes}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, series = {LIPIcs}, title = {{Global} {Caching} for the {Alternation}-free {Coalgebraic} mu-calculus}, url = {http://drops.dagstuhl.de/opus/volltexte/2016/6172/}, venue = {Québec City, Canada}, volume = {59}, year = {2016} } @inproceedings{faucris.107509644, address = {Dagstuhl}, author = {Hausmann, Daniel and Schröder, Lutz and Egger, Christoph}, booktitle = {27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada}, date = {2016-08-23/2016-08-26}, doi = {10.4230/LIPIcs.CONCUR.2016.34}, editor = {Josée Desharnais, Radha Jagadeesan}, faupublication = {yes}, isbn = {978-3-95977-017-0}, keywords = {Fixpoint logics; temporal logics; automated reasoning; coalgebraic logic; mu-calculus}, pages = {34:1--34:15}, peerreviewed = {Yes}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, series = {LIPIcs}, title = {{Global} {Caching} for the {Alternation}-free mu-{Calculus}}, url = {http://www.dagstuhl.de/dagpub/978-3-95977-017-0}, venue = {Québec City}, volume = {59}, year = {2016} } @inproceedings{faucris.203762390, abstract = {Branching-time temporal logics generalizing relational temporal logics such as CTL have been proposed for various system types beyond the purely relational world. This includes, e.g., alternating-time logics, which talk about winning strategies over concurrent game structures, and Parikh's game logic, which is interpreted over monotone neighbourhood frames, as well as probabilistic fixpoint logics. Coalgebraic logic has emerged as a unifying semantic and algorithmic framework for logics featuring generalized modalities of this type. Here, we present a generic global caching algorithm for satisfiability checking in the flat coalgebraic mu-calculus, which realizes known tight exponential-time upper complexity bounds but offers potential for heuristic optimization. It is based on a tableau system that makes do without additional labelling of nodes beyond formulas from the standard Fischer-Ladner closure, such as foci or termination counters for eventualities. Moreover, the tableau system is single-pass, i.e. avoids building an exponential-sized structure in a first pass; to our best knowledge, optimal single-pass systems without numeric time-outs were not previously available even for CTL.}, author = {Hausmann, Daniel and Schröder, Lutz}, booktitle = {Proc. 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015}, doi = {10.1109/TIME.2015.15}, faupublication = {yes}, keywords = {fixpoint logics;satisfiability;coalgebraic logic;global caching}, month = {Jan}, pages = {121-130}, peerreviewed = {Yes}, publisher = {IEEE}, title = {{Global} {Caching} for the {Flat} {Coalgebraic} mu-{Calculus}}, year = {2015} } @inproceedings{faucris.107669584, abstract = {Branching-time temporal logics generalizing relational temporal logics such as CTL have been proposed for various system types beyond the purely relational world. This includes, e.g., alternating-time logics, which talk about winning strategies over concurrent game structures, and Parikh’s game logic, which is interpreted over monotone neighbourhood frames, as well as probabilistic fixpoint logics. Coalgebraic logic has emerged as a unifying semantic and algorithmic framework for logics featuring generalized modalities of this type. Here, we present a generic global caching algorithm for satisfiability checking in the flat coalgebraic mu-calculus, which realizes known tight exponential-time upper complexity bounds but offers potential for heuristic optimization. It is based on a tableau system that makes do without additional labelling of nodes beyond formulas from the standard Fischer-Ladner closure, such as foci or termination counters for eventualities. Moreover, the tableau system is singlepass, i.e. avoids building an exponential-sized structure in a first pass; to our best knowledge, optimal single-pass systems without numeric time-outs were not previously available even for CT}, address = {Berlin}, author = {Hausmann, Daniel and Schröder, Lutz}, booktitle = {Proceedings, 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015}, date = {2015-09-23/2015-09-25}, doi = {10.1109/TIME.2015.15}, editor = {Grandi F, Lange M, Lomuscio A}, faupublication = {yes}, isbn = {978-1-4673-9317-1}, keywords = {Fixpoint logic; coalgebraic logic; global caching; fixpoint logic}, pages = {121-130}, peerreviewed = {Yes}, publisher = {Springer}, title = {{Global} {Caching} for the {Flat} {Coalgebraic} μ-{Calculus}}, venue = {Kassel}, year = {2015} } @inproceedings{faucris.281406173, abstract = {The framework of graded semantics uses graded monads to capture behavioural equivalences of varying granularity, for example as found in the linear-time / branching-time spectrum, over general system types. We describe a generic Spoiler-Duplicator game for graded semantics that is extracted from the given graded monad, and may be seen as playing out an equational proof; instances include standard pebble games for simulation and bisimulation as well as games for trace-like equivalences and coalgebraic behavioural equivalence. Considerations on an infnite variant of such games lead to a novel notion of infnite-depth graded semantics. Under reasonable restrictions, the infnite-depth graded semantics associated to a given graded equivalence can be characterized in terms of a determinization construction for coalgebras under the equivalence at hand.}, author = {Ford, Matthew and Milius, Stefan and Schröder, Lutz and Beohar, Harsh and König, Barbara}, booktitle = {Proceedings - Symposium on Logic in Computer Science}, date = {2022-08-02/2022-08-05}, doi = {10.1145/3531130.3533374}, faupublication = {yes}, isbn = {9781450393515}, keywords = {Behavioural equivalence; Games; Graded monads; Lineartime/branching-time spectrum; Semantics}, note = {CRIS-Team Scopus Importer:2022-09-09}, peerreviewed = {unknown}, publisher = {Institute of Electrical and Electronics Engineers Inc.}, title = {{Graded} {Monads} and {Behavioural} {Equivalence} {Games}}, venue = {Haifa, ISR}, year = {2022} } @inproceedings{faucris.226669056, abstract = {State-based models of concurrent systems are traditionally considered under a variety of notions of process equivalence. In the case of labelled transition systems, these equivalences range from trace equivalence to (strong) bisimilarity, and are organized in what is known as the linear time – branching time spectrum. A combination of universal coalgebra and graded monads provides a generic framework in which the semantics of concurrency can be parametrized both over the branching type of the underlying transition systems and over the granularity of process equivalence. We show in the present paper that this framework of graded semantics does subsume the most important equivalences from the linear time – branching time spectrum. An important feature of graded semantics is that it allows for the principled extraction of characteristic modal logics. We have established invariance of these graded logics under the given graded semantics in earlier work; in the present paper, we extend the logical framework with an explicit propositional layer and provide a generic expressiveness criterion that generalizes the classical Hennessy-Milner theorem to coarser notions of process equivalence. We extract graded logics for a range of graded semantics on labelled transition systems and probabilistic systems, and give exemplary proofs of their expressiveness based on our generic criterion.}, author = {Dorsch, Ulrich and Milius, Stefan and Schröder, Lutz}, booktitle = {Leibniz International Proceedings in Informatics, LIPIcs}, date = {2019-08-27/2019-08-30}, doi = {10.4230/LIPIcs.CONCUR.2019.36}, editor = {Wan Fokkink, Rob van Glabbeek}, faupublication = {yes}, isbn = {9783959771214}, keywords = {Branching Time; Expressiveness; Linear Time; Modal Logics; Monads; System Equivalences}, note = {CRIS-Team Scopus Importer:2019-09-17}, peerreviewed = {unknown}, publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing}, title = {{Graded} monads and graded logics for the linear time – {Branching} time spectrum}, venue = {Amsterdam}, volume = {140}, year = {2019} } @article{faucris.224375990, abstract = {Models of iterated computation, such as (completely) iterative monads, often depend on a notion of guardedness, which guarantees unique solvability of recursive equations and requires roughly that recursive calls happen only under certain guarding operations. On the other hand, many models of iteration do admit unguarded iteration. Solutions are then no longer unique, and in general not even determined as least or greatest fixpoints, being instead governed by quasi-equational axioms. Monads that support unguarded iteration in this sense are called (complete) Elgot monads. Here, we propose to equip (Kleisli categories of) monads with an abstract notion of guardedness and then require solvability of abstractly guarded recursive equations; examples of such abstractly guarded pre-iterative monads include both iterative monads and Elgot monads, the latter by deeming any recursive definition to be abstractly guarded. Our main result is then that Elgot monads are precisely the iteration-congruent retracts of abstractly guarded iterative monads, the latter being defined as admitting unique solutions of abstractly guarded recursive equations; in other words, models of unguarded iteration come about by quotienting models of guarded iteration.}, author = {Goncharov, Sergey and Schröder, Lutz and Rauch, Christoph and Pirog, Maciej}, doi = {10.23638/LMCS-15(3:1)2019}, faupublication = {yes}, journal = {Logical Methods in Computer Science}, month = {Jan}, note = {CRIS-Team WoS Importer:2019-08-13}, peerreviewed = {Yes}, title = {{Guarded} and {Unguarded} {Iteration} for {Generalized} {Processes}}, volume = {15}, year = {2019} } @inproceedings{faucris.203763967, author = {Goncharov, Sergey and Schröder, Lutz}, booktitle = {21st International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018}, doi = {10.1007/978-3-319-89366-2{\_}17}, faupublication = {yes}, isbn = {9783319893655}, pages = {313-330}, peerreviewed = {Yes}, publisher = {Springer Verlag}, series = {Lecture Notes in Computer Science}, title = {{Guarded} {Traced} {Categories}}, year = {2018} } @inproceedings{faucris.311727087, abstract = {We present a higher-order extension of Turi and Plotkin's abstract GSOS framework that retains the key feature of the latter: for every language whose operational rules are represented by a higher-order GSOS law, strong bisimilarity on the canonical operational model is a congruence with respect to the operations of the language. We further extend this result to weak (bi-)similarity, for which a categorical account of Howe's method is developed. It encompasses, for instance, Abramsky's classical compositionality theorem for applicative similarity in the untyped λ-calculus. In addition, we give first steps of a theory of logical relations at the level of higher-order abstract GSOS.}, author = {Goncharov, Sergey and Milius, Stefan and Schröder, Lutz and Tsampas, Stylianos and Urbat, Henning}, booktitle = {Leibniz International Proceedings in Informatics, LIPIcs}, date = {2023-06-19/2023-06-21}, doi = {10.4230/LIPIcs.CALCO.2023.24}, editor = {Paolo Baldan, Valeria de Paiva}, faupublication = {yes}, isbn = {9783959772877}, keywords = {Abstract GSOS; applicative bisimilarity; bialgebra; lambda-calculus}, note = {CRIS-Team Scopus Importer:2023-10-06}, peerreviewed = {unknown}, publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing}, title = {{Higher}-{Order} {Mathematical} {Operational} {Semantics}}, venue = {Bloomington, IN, USA}, volume = {270}, year = {2023} } @article{faucris.113624324, abstract = {Common estimation algorithms, such as least squares estimation or the Kalman filter, operate on a state in a state space S that is represented as a real-valued vector. However, for many quantities, most notably orientations in 3D, S is not a vector space, but a so-called manifold, i.e. it behaves like a vector space locally but has a more complex global topological structure. For integrating these quantities, several ad hoc approaches have been proposed. Here, we present a principled solution to this problem where the structure of the manifold S is encapsulated by two operators, state displacement: S×

global assumptions in coalgebraic modal logics. Unlike earlier

results of this kind, we do not require a tractable set of tableau

rules for the instance logics, so that the result applies to wider

classes of logics. Examples are Presburger modal logic,

which extends graded modal logic with linear inequalities over

numbers of successors, and probabilistic modal logic with polynomial

inequalities over probabilities. We establish the theoretical upper

bound using a type elimination algorithm. We also provide a global

caching algorithm that offers potential for practical reasoning.

}, address = {Berlin}, author = {Kupke, Clemens and Pattinson, Dirk and Schröder, Lutz}, booktitle = {Fundamentals of Computation Theory - 20th International Symposium, FCT 2015, Proceedings}, date = {2015-08-17/2015-08-19}, doi = {10.1007/978-3-319-22177-9{\_}28}, faupublication = {yes}, keywords = {Modal logic; tableaux; global caching; Presburger modalities; coalgebraic logic}, pages = {367--380}, peerreviewed = {Yes}, publisher = {Springer}, title = {{Reasoning} with {Global} {Assumptions} in {Arithmetic} {Modal} {Logics}}, venue = {Gdansk}, year = {2015} } @article{faucris.244832898, abstract = {Social media are of paramount importance to public discourse. RANT aims to contribute methods and formalisms for extracting, representing, and processing arguments from noisy text found in social media discussions, using a large corpus of pre-referendum Brexit tweets as a running case study. We identify recurring linguistic argumentation patterns in a corpus-linguistic analysis and formulate corresponding corpus queries to extract arguments automatically. Given the huge amount of social media data available, our approach aims at high precision at the possible price of low recall. Argumentation patterns are directly associated with logical patterns in a dedicated formalism and accordingly, individual arguments are directly parsed as logical formulae. The logical formalism for argument representation features a broad range of modalities capturing real-life modes of expression. We cast this formalism as a family of instance logics in the generic framework of coalgebraic logic and complement it by a flexible framework to represent relationships between arguments; including standard relations like attack and support but also relations extracted from metadata. Some relations are inferred from the logical content of individual arguments. We are in the process of developing suitable generalizations of various extension semantics for argumentation frameworks combined with corresponding algorithmic methods to allow for the automated retrieval of large-scale argumentative positions.

op, model state spaces with algebraic access operations. Standard equational reasoning is known to be sound but incomplete for comodels. We give two sound and complete calculi for equational reasoning over comodels: an inductive calculus for equality-on-the-nose, and a coinductive/inductive calculus for equality modulo bisimulation which captures bisimulations syntactically through non-wellfounded proofs.}, author = {Schröder, Lutz and Pattinson, Dirk}, booktitle = {Proc. Mathematical Foundations of Programming Semantics XXXI, MFPS 2015}, doi = {10.1016/j.entcs.2015.12.019}, faupublication = {yes}, keywords = {Equational Logic, Comodels, Completeness, Bisimulation}, note = {UnivIS-Import:2016-02-10:Pub.2015.tech.IMMD.profes{\_}1.sounda}, pages = {315-331}, peerreviewed = {Yes}, publisher = {Elsevier BV}, series = {Electronic Notes in Theoretical Computer Science}, title = {{Sound} and {Complete} {Equational} {Reasoning} over {Comodels}}, url = {http://www8.cs.fau.de/{\_}media/research:papers:comodels-compl.pdf}, venue = {Nijmegen}, volume = {319}, year = {2015} } @inproceedings{faucris.278507091, abstract = {Compositionality of denotational semantics is an important concern in programming semantics. Mathematical operational semantics in the sense of Turi and Plotkin guarantees compositionality, but seen from the point of view of stateful computation it applies only to very fine-grained equivalences that essentially assume unrestricted interference by the environment between any two statements. We introduce the more restrictive stateful SOS rule format for stateful languages. We show that compositionality of two more coarse-grained semantics, respectively given by assuming read-only interference or no interference between steps, remains an undecidable property even for stateful SOS. However, further restricting the rule format in a manner inspired by the cool GSOS formats of Bloom and van Glabbeek, we obtain the streamlined and cool stateful SOS formats, which respectively guarantee compositionality of the two more abstract equivalences.}, author = {Goncharov, Sergey and Milius, Stefan and Schröder, Lutz and Tsampas, Stelios and Urbat, Henning}, booktitle = {Leibniz International Proceedings in Informatics, LIPIcs}, date = {2022-08-02/2022-08-05}, doi = {10.4230/LIPIcs.FSCD.2022.30}, editor = {Amy P. Felty}, faupublication = {yes}, isbn = {9783959772334}, keywords = {Distributive Laws; Rule Formats; Structural Operational Semantics}, note = {CRIS-Team Scopus Importer:2022-07-22}, peerreviewed = {unknown}, publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing}, title = {{Stateful} {Structural} {Operational} {Semantics}}, venue = {Haifa, ISR}, volume = {228}, year = {2022} } @inproceedings{faucris.114030664, abstract = {While reasoning in a logic extending a complete Boolean basis is coNP-hard, re- stricting to conjunctive fragments of modal languages sometimes allows for tractable reasoning even in the presence of greatest fixpoints. One such example is the EL family of description logics; here, eficient reasoning is based on satisfaction checking in suitable small models that characterize formulas in terms of simulations. It is well- known, though, that not every conjunctive modal language has a tractable reasoning problem. Natural questions are then how common such tractable fragments are and how to identify them. In this work we provide suficient conditions for tractability in a general way by considering unlabeled tableau rules for a given modal logic. We work in the framework of coalgebraic modal logics as unifying semantic setting. Apart from recovering known results for description logics such as and