-
On Kleisli liftings and decorated trace semantics
Authors:
Daniel Luckhardt,
Harsh Beohar,
Sebastian Küpper
Abstract:
It is well known that Kleisli categories provide a natural language to model side effects. For instance, in the theory of coalgebras, behavioural equivalence coincides with language equivalence (instead of bisimilarity) when nondeterministic automata are modelled as coalgebras living in the Kleisli category of the powerset monad. In this paper, our aim is to establish decorated trace semantics bas…
▽ More
It is well known that Kleisli categories provide a natural language to model side effects. For instance, in the theory of coalgebras, behavioural equivalence coincides with language equivalence (instead of bisimilarity) when nondeterministic automata are modelled as coalgebras living in the Kleisli category of the powerset monad. In this paper, our aim is to establish decorated trace semantics based on language and ready equivalences for conditional transition systems (CTSs) with/without upgrades. To this end, we model CTSs as coalgebras living in the Kleisli category of a relative monad. Our results are twofold. First, we reduce the problem of defining a Kleisli lifting for the machine endofunctor in the context of a relative monad to the classical notion of Kleisli lifting. Second, we provide a recipe based on indexed categories to construct a Kleisli lifting for general endofunctors.
△ Less
Submitted 7 December, 2024; v1 submitted 13 November, 2024;
originally announced November 2024.
-
ELRA: Exponential learning rate adaption gradient descent optimization method
Authors:
Alexander Kleinsorge,
Stefan Kupper,
Alexander Fauck,
Felix Rothe
Abstract:
We present a novel, fast (exponential rate adaption), ab initio (hyper-parameter-free) gradient based optimizer algorithm. The main idea of the method is to adapt the learning rate $α$ by situational awareness, mainly striving for orthogonal neighboring gradients. The method has a high success and fast convergence rate and does not rely on hand-tuned parameters giving it greater universality. It c…
▽ More
We present a novel, fast (exponential rate adaption), ab initio (hyper-parameter-free) gradient based optimizer algorithm. The main idea of the method is to adapt the learning rate $α$ by situational awareness, mainly striving for orthogonal neighboring gradients. The method has a high success and fast convergence rate and does not rely on hand-tuned parameters giving it greater universality. It can be applied to problems of any dimensions n and scales only linearly (of order O(n)) with the dimension of the problem. It optimizes convex and non-convex continuous landscapes providing some kind of gradient. In contrast to the Ada-family (AdaGrad, AdaMax, AdaDelta, Adam, etc.) the method is rotation invariant: optimization path and performance are independent of coordinate choices. The impressive performance is demonstrated by extensive experiments on the MNIST benchmark data-set against state-of-the-art optimizers. We name this new class of optimizers after its core idea Exponential Learning Rate Adaption - ELRA. We present it in two variants c2min and p2min with slightly different control. The authors strongly believe that ELRA will open a completely new research direction for gradient descent optimize.
△ Less
Submitted 12 September, 2023;
originally announced September 2023.
-
Predicate and relation liftings for coalgebras with side effects: an application in coalgebraic modal logic
Authors:
H. Beohar,
B. König,
S. Küpper,
C. Mika-Michalski
Abstract:
We study coalgebraic modal logic to characterise behavioural equivalence in the presence of side effects, i.e., when coalgebras live in a (co)Kleisli or an Eilenberg-Moore category. Our aim is to develop a general framework based on indexed categories/fibrations that is common to the aforementioned categories. In particular, we show how the coalgebraic notion of behavioural equivalence arises from…
▽ More
We study coalgebraic modal logic to characterise behavioural equivalence in the presence of side effects, i.e., when coalgebras live in a (co)Kleisli or an Eilenberg-Moore category. Our aim is to develop a general framework based on indexed categories/fibrations that is common to the aforementioned categories. In particular, we show how the coalgebraic notion of behavioural equivalence arises from a relation lifting (a special kind of indexed morphism) and we give a general recipe to construct such liftings in the above three cases. Lastly, we apply this framework to derive logical characterisations for (weighted) language equivalence and conditional bisimilarity.
△ Less
Submitted 4 February, 2022; v1 submitted 19 October, 2021;
originally announced October 2021.
-
What Makes Agile Software Development Agile?
Authors:
Marco Kuhrmann,
Paolo Tell,
Regina Hebig,
Jil Klünder,
Jürgen Münch,
Oliver Linssen,
Dietmar Pfahl,
Michael Felderer,
Christian R. Prause,
Stephen G. MacDonell,
Joyce Nakatumba-Nabende,
David Raffo,
Sarah Beecham,
Eray Tüzün,
Gustavo López,
Nicolas Paez,
Diego Fontdevila,
Sherlock A. Licorish,
Steffen Küpper,
Günther Ruhe,
Eric Knauss,
Özden Özcan-Top,
Paul Clarke,
Fergal McCaffery,
Marcela Genero
, et al. (22 additional authors not shown)
Abstract:
Together with many success stories, promises such as the increase in production speed and the improvement in stakeholders' collaboration have contributed to making agile a transformation in the software industry in which many companies want to take part. However, driven either by a natural and expected evolution or by contextual factors that challenge the adoption of agile methods as prescribed by…
▽ More
Together with many success stories, promises such as the increase in production speed and the improvement in stakeholders' collaboration have contributed to making agile a transformation in the software industry in which many companies want to take part. However, driven either by a natural and expected evolution or by contextual factors that challenge the adoption of agile methods as prescribed by their creator(s), software processes in practice mutate into hybrids over time. Are these still agile? In this article, we investigate the question: what makes a software development method agile? We present an empirical study grounded in a large-scale international survey that aims to identify software development methods and practices that improve or tame agility. Based on 556 data points, we analyze the perceived degree of agility in the implementation of standard project disciplines and its relation to used development methods and practices. Our findings suggest that only a small number of participants operate their projects in a purely traditional or agile manner (under 15%). That said, most project disciplines and most practices show a clear trend towards increasing degrees of agility. Compared to the methods used to develop software, the selection of practices has a stronger effect on the degree of agility of a given discipline. Finally, there are no methods or practices that explicitly guarantee or prevent agility. We conclude that agility cannot be defined solely at the process level. Additional factors need to be taken into account when trying to implement or improve agility in a software company. Finally, we discuss the field of software process-related research in the light of our findings and present a roadmap for future research.
△ Less
Submitted 23 September, 2021;
originally announced September 2021.
-
Towards the statistical construction of hybrid development methods
Authors:
Paolo Tell,
Jil Klünder,
Steffen Küpper,
David Raffo,
Stephen MacDonell,
Jürgen Münch,
Dietmar Pfahl,
Oliver Linssen,
Marco Kuhrmann
Abstract:
Hardly any software development process is used as prescribed by authors or standards. Regardless of company size or industry sector, a majority of project teams and companies use hybrid development methods (short: hybrid methods) that combine different development methods and practices. Even though such hybrid methods are highly individualized, a common understanding of how to systematically cons…
▽ More
Hardly any software development process is used as prescribed by authors or standards. Regardless of company size or industry sector, a majority of project teams and companies use hybrid development methods (short: hybrid methods) that combine different development methods and practices. Even though such hybrid methods are highly individualized, a common understanding of how to systematically construct synergetic practices is missing. In this article, we make a first step towards a statistical construction procedure for hybrid methods. Grounded in 1467 data points from a large-scale practitioner survey, we study the question: What are hybrid methods made of and how can they be systematically constructed? Our findings show that only eight methods and few practices build the core of modern software development. Using an 85% agreement level in the participants' selections, we provide examples illustrating how hybrid methods can be characterized by the practices they are made of. Furthermore, using this characterization, we develop an initial construction procedure, which allows for defining a method frame and enriching it incrementally to devise a hybrid method using ranked sets of practice.
△ Less
Submitted 27 May, 2021;
originally announced May 2021.
-
Catching up with Method and Process Practice: An Industry-Informed Baseline for Researchers
Authors:
Jil Klünder,
Regina Hebig,
Paolo Tell,
Marco Kuhrmann,
Joyce Nakatumba-Nabende,
Rogardt Heldal,
Stephan Krusche,
Masud Fazal-Baqaie,
Michael Felderer,
Marcela Fabiana Genero Bocco,
Steffen Küpper,
Sherlock A. Licorish,
Gustavo Lòpez,
Fergal McCaffery,
Özden Özcan Top,
Christian R. Prause,
Rafael Prikladnicki,
Eray Tüzün,
Dietmar Pfahl,
Kurt Schneider,
Stephen G. MacDonell
Abstract:
Software development methods are usually not applied by the book. Companies are under pressure to continuously deploy software products that meet market needs and stakeholders' requests. To implement efficient and effective development processes, companies utilize multiple frameworks, methods and practices, and combine these into hybrid methods. A common combination contains a rich management fram…
▽ More
Software development methods are usually not applied by the book. Companies are under pressure to continuously deploy software products that meet market needs and stakeholders' requests. To implement efficient and effective development processes, companies utilize multiple frameworks, methods and practices, and combine these into hybrid methods. A common combination contains a rich management framework to organize and steer projects complemented with a number of smaller practices providing the development teams with tools to complete their tasks. In this paper, based on 732 data points collected through an international survey, we study the software development process use in practice. Our results show that 76.8% of the companies implement hybrid methods. Company size as well as the strategy in devising and evolving hybrid methods affect the suitability of the chosen process to reach company or project goals. Our findings show that companies that combine planned improvement programs with process evolution can increase their process' suitability by up to 5%.
△ Less
Submitted 28 January, 2021;
originally announced January 2021.
-
What are Hybrid Development Methods Made Of? An Evidence-based Characterization
Authors:
Paolo Tell,
Jil Klünder,
Steffen Küpper,
David Raffo,
Stephen G. MacDonell,
Jürgen Münch,
Dietmar Pfahl,
Oliver Linssen,
Marco Kuhrmann
Abstract:
Among the multitude of software development processes available, hardly any is used by the book. Regardless of company size or industry sector, a majority of project teams and companies use customized processes that combine different development methods -- so-called hybrid development methods. Even though such hybrid development methods are highly individualized, a common understanding of how to s…
▽ More
Among the multitude of software development processes available, hardly any is used by the book. Regardless of company size or industry sector, a majority of project teams and companies use customized processes that combine different development methods -- so-called hybrid development methods. Even though such hybrid development methods are highly individualized, a common understanding of how to systematically construct synergetic practices is missing. In this paper, we make a first step towards devising such guidelines. Grounded in 1,467 data points from a large-scale online survey among practitioners, we study the current state of practice in process use to answer the question: What are hybrid development methods made of? Our findings reveal that only eight methods and few practices build the core of modern software development. This small set allows for statistically constructing hybrid development methods. Using an 85% agreement level in the participants' selections, we provide two examples illustrating how hybrid development methods are characterized by the practices they are made of. Our evidence-based analysis approach lays the foundation for devising hybrid development methods.
△ Less
Submitted 20 January, 2021;
originally announced January 2021.
-
Conditional Bisimilarity for Reactive Systems
Authors:
Mathias Hülsbusch,
Barbara König,
Sebastian Küpper,
Lara Stoltenow
Abstract:
Reactive systems à la Leifer and Milner, an abstract categorical framework for rewriting, provide a suitable framework for deriving bisimulation congruences. This is done by synthesizing interactions with the environment in order to obtain a compositional semantics.
We enrich the notion of reactive systems by conditions on two levels: first, as in earlier work, we consider rules enriched with…
▽ More
Reactive systems à la Leifer and Milner, an abstract categorical framework for rewriting, provide a suitable framework for deriving bisimulation congruences. This is done by synthesizing interactions with the environment in order to obtain a compositional semantics.
We enrich the notion of reactive systems by conditions on two levels: first, as in earlier work, we consider rules enriched with application conditions and second, we investigate the notion of conditional bisimilarity. Conditional bisimilarity allows us to say that two system states are bisimilar provided that the environment satisfies a given condition.
We present several equivalent definitions of conditional bisimilarity, including one that is useful for concrete proofs and that employs an up-to-context technique, and we compare with related behavioural equivalences. We consider examples based on DPO graph rewriting, an instantiation of reactive systems.
△ Less
Submitted 11 January, 2022; v1 submitted 24 April, 2020;
originally announced April 2020.
-
Bisimulation maps in presheaf categories
Authors:
Harsh Beohar,
Sebastian Küpper
Abstract:
The category of presheaves on a (small) category is a suitable semantic universe to study behaviour of various dynamical systems. In particular, presheaves can be used to record the executions of a system and their morphisms correspond to simulation maps for various kinds of state-based systems. In this paper, we introduce a notion of bisimulation maps between presheaves (or executions) to capture…
▽ More
The category of presheaves on a (small) category is a suitable semantic universe to study behaviour of various dynamical systems. In particular, presheaves can be used to record the executions of a system and their morphisms correspond to simulation maps for various kinds of state-based systems. In this paper, we introduce a notion of bisimulation maps between presheaves (or executions) to capture well known behavioural equivalences in an abstract way. We demonstrate the versatility of this framework by working out the characterisations for standard bisimulation, $\forall$-fair bisimulation, and branching bisimulation.
△ Less
Submitted 4 September, 2019;
originally announced September 2019.
-
PAWS: A Tool for the Analysis of Weighted Systems
Authors:
Barbara König,
Sebastian Küpper,
Christina Mika
Abstract:
PAWS is a tool to analyse the behaviour of weighted automata and conditional transition systems. At its core PAWS is based on a generic implementation of algorithms for checking language equivalence in weighted automata and bisimulation in conditional transition systems. This architecture allows for the use of arbitrary user-defined semirings. New semirings can be generated during run-time and the…
▽ More
PAWS is a tool to analyse the behaviour of weighted automata and conditional transition systems. At its core PAWS is based on a generic implementation of algorithms for checking language equivalence in weighted automata and bisimulation in conditional transition systems. This architecture allows for the use of arbitrary user-defined semirings. New semirings can be generated during run-time and the user can rely on numerous automatisation techniques to create new semiring structures for PAWS' algorithms. Basic semirings such as distributive complete lattices and fields of fractions can be defined by specifying few parameters, more exotic semirings can be generated from other semirings or defined from scratch using a built-in semiring generator. In the most general case, users can define new semirings by programming (in C#) the base operations of the semiring and a procedure to solve linear equations and use their newly generated semiring in the analysis tools that PAWS offers.
△ Less
Submitted 13 July, 2017;
originally announced July 2017.
-
Conditional Transition Systems with Upgrades
Authors:
Harsh Beohar,
Barbara König,
Sebastian Küpper,
Alexandra Silva
Abstract:
We introduce a variant of transition systems, where activation of transitions depends on conditions of the environment and upgrades during runtime potentially create additional transitions. Using a cornerstone result in lattice theory, we show that such transition systems can be modelled in two ways: as conditional transition systems (CTS) with a partial order on conditions, or as lattice transiti…
▽ More
We introduce a variant of transition systems, where activation of transitions depends on conditions of the environment and upgrades during runtime potentially create additional transitions. Using a cornerstone result in lattice theory, we show that such transition systems can be modelled in two ways: as conditional transition systems (CTS) with a partial order on conditions, or as lattice transition systems (LaTS), where transitions are labelled with the elements from a distributive lattice. We define equivalent notions of bisimilarity for both variants and characterise them via a bisimulation game.
We explain how conditional transition systems are related to featured transition systems for the modelling of software product lines. Furthermore, we show how to compute bisimilarity symbolically via BDDs by defining an operation on BDDs that approximates an element of a Boolean algebra into a lattice. We have implemented our procedure and provide runtime results.
△ Less
Submitted 8 June, 2017;
originally announced June 2017.
-
On path-based coalgebras and weak notions of bisimulation
Authors:
Harsh Beohar,
Sebastian Küpper
Abstract:
It is well known that the theory of coalgebras provides an abstract definition of behavioural equivalence that coincides with strong bisimulation across a wide variety of state-based systems. Unfortunately, the theory in the presence of so-called silent actions is not yet fully developed. In this paper, we give a coalgebraic characterisation of branching bisimulation in the context of labelled tra…
▽ More
It is well known that the theory of coalgebras provides an abstract definition of behavioural equivalence that coincides with strong bisimulation across a wide variety of state-based systems. Unfortunately, the theory in the presence of so-called silent actions is not yet fully developed. In this paper, we give a coalgebraic characterisation of branching bisimulation in the context of labelled transition systems and fully probabilistic systems. It is shown that recording executions (up to a notion of stuttering), rather than the set of successor states, from a state is sufficient to characterise branching bisimulation in both cases.
△ Less
Submitted 30 May, 2017; v1 submitted 24 May, 2017;
originally announced May 2017.
-
Up-To Techniques for Weighted Systems (Extended Version)
Authors:
Filippo Bonchi,
Barbara König,
Sebastian Küpper
Abstract:
We show how up-to techniques for (bi-)similarity can be used in the setting of weighted systems. The problems we consider are language equivalence, language inclusion and the threshold problem (also known as universality problem) for weighted automata. We build a bisimulation relation on the fly and work up-to congruence and up-to similarity. This requires to determine whether a pair of vectors (o…
▽ More
We show how up-to techniques for (bi-)similarity can be used in the setting of weighted systems. The problems we consider are language equivalence, language inclusion and the threshold problem (also known as universality problem) for weighted automata. We build a bisimulation relation on the fly and work up-to congruence and up-to similarity. This requires to determine whether a pair of vectors (over a semiring) is in the congruence closure of a given relation of vectors. This problem is considered for rings and l-monoids, for the latter we provide a rewriting algorithm and show its confluence and termination. We then explain how to apply these up-to techniques to weighted automata and provide runtime results.
△ Less
Submitted 23 January, 2017; v1 submitted 18 January, 2017;
originally announced January 2017.
-
A coalgebraic treatment of conditional transition systems with upgrades
Authors:
Harsh Beohar,
Barbara König,
Sebastian Küpper,
Alexandra Silva,
Thorsten Wißmann
Abstract:
We consider conditional transition systems, that model software product lines with upgrades, in a coalgebraic setting. By using Birkhoff's duality for distributive lattices, we derive two equivalent Kleisli categories in which these coalgebras live: Kleisli categories based on the reader and on the so-called lattice monad over $\mathsf{Poset}$. We study two different functors describing the branch…
▽ More
We consider conditional transition systems, that model software product lines with upgrades, in a coalgebraic setting. By using Birkhoff's duality for distributive lattices, we derive two equivalent Kleisli categories in which these coalgebras live: Kleisli categories based on the reader and on the so-called lattice monad over $\mathsf{Poset}$. We study two different functors describing the branching type of the coalgebra and investigate the resulting behavioural equivalence. Furthermore we show how an existing algorithm for coalgebra minimisation can be instantiated to derive behavioural equivalences in this setting.
△ Less
Submitted 15 December, 2018; v1 submitted 15 December, 2016;
originally announced December 2016.
