arXiv subjects

Lutz Schröder

Publications and source records attributed to Lutz Schröder.

84 records · Page 5Linked to original sources

arXiv2013

Towards Ontological Support for Principle Solutions in Mechanical Engineering

The engineering design process follows a series of standardized stages of development, which have many aspects in common with software engineering. Among these stages, the principle solution can be regarded as an analogue of the design specification, fixing as it does the way the final product works. It is usually constructed as an abstract sketch (hand-drawn or constructed with a CAD system) where the functional parts of the product are identified, and geometric and topological constraints are formulated. Here, we outline a semantic approach where the principle solution is annotated with ontological assertions, thus making the intended requirements explicit and available for further machine processing; this includes the automated detection of design errors in the final CAD model, making additional use of a background ontology of engineering knowledge. We embed this approach into a document-oriented design workflow, in which the background ontology and semantic annotations in the documents are exploited to trace parts and requirements through the design process and across different applications.

cs.SE↗

arXiv2013

Exploring the Boundaries of Monad Tensorability on Set

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.

cs.LO↗

arXiv2013

Simulations and Bisimulations For Coalgebraic Modal Logics

We define a notion of Lambda-simulation for coalgebraic modal logics, parametric on the choice Lambda of predicate liftings for a functor T. We show this notion is adequate in several ways: i) it preserves truth of positive formulas, ii) for Lambda a separating set of monotone predicate liftings, the associated notion of Lambda-bisimulation corresponds to T-behavioural equivalence (moreover Lambda-n-bisimulations correspond to T-n-behavioural equivalence), and iii) in fact, for Lambda-separating and T preserving weak pullbacks, difunctional Lambda-bisimulations are T-bisimulations. In essence, we arrive at a modular notion of equivalence that, when used with a separating set of monotone predicate liftings, coincides with T-behavioural equivalence regardless of whether T preserves weak pullbacks (unlike the notion of T-bisimilarity).

cs.LO↗

arXiv2011

Integrating Generic Sensor Fusion Algorithms with Sound State Representations through Encapsulation of Manifolds

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 x R^n --> S and its inverse [-]: S x S --> R^n. These operators provide a local vector-space view δ; --> x [+] δ; around a given state x. Generic estimation algorithms can then work on the manifold S mainly by replacing +/- with [+]/[-] where appropriate. We analyze these operators axiomatically, and demonstrate their use in least-squares estimation and the Unscented Kalman Filter. Moreover, we exploit the idea of encapsulation from a software engineering perspective in the Manifold Toolkit, where the [+]/[-] operators mediate between a "flat-vector" view for the generic algorithm and a "named-members" view for the problem specific functions.

cs.RO↗

arXiv2011

A Coinductive Calculus for Asynchronous Side-effecting Processes

We present an abstract framework for concurrent processes in which atomic steps have generic side effects, handled according to the principle of monadic encapsulation of effects. Processes in this framework are potentially infinite resumptions, modelled using final coalgebras over the monadic base. As a calculus for such processes, we introduce a concurrent extension of Moggi's monadic metalanguage of effects. We establish soundness and completeness of a natural equational axiomatisation of this calculus. Moreover, we identify a corecursion scheme that is explicitly definable over the base language and provides flexible expressive means for the definition of new operators on processes, such as parallel composition. As a worked example, we prove the safety of a generic mutual exclusion scheme using a verification logic built on top of the equational calculus.

cs.LO↗

arXiv2011

Powermonads and Tensors of Unranked Effects

In semantics and in programming practice, algebraic concepts such as monads or, essentially equivalently, (large) Lawvere theories are a well-established tool for modelling generic side-effects. An important issue in this context are combination mechanisms for such algebraic effects, which allow for the modular design of programming languages and verification logics. The most basic combination operators are sum and tensor: while the sum of effects is just their non-interacting union, the tensor imposes commutation of effects. However, for effects with unbounded arity, such as continuations or unbounded nondeterminism, it is not a priori clear whether these combinations actually exist in all cases. Here, we introduce the class of uniform effects, which includes unbounded nondeterminism and continuations, and prove that the tensor does always exist if one of the component effects is uniform, thus in particular improving on previous results on tensoring with continuations. We then treat the case of nondeterminism in more detail, and give an order-theoretic characterization of effects for which tensoring with nondeterminism is conservative, thus enabling nondeterministic arguments such as a generic version of the Fischer-Ladner encoding of control operators.

cs.LO↗

arXiv2011

Generic Modal Cut Elimination Applied to Conditional Logics

We develop a general criterion for cut elimination in sequent calculi for propositional modal logics, which rests on absorption of cut, contraction, weakening and inversion by the purely modal part of the rule system. Our criterion applies also to a wide variety of logics outside the realm of normal modal logic. We give extensive example instantiations of our framework to various conditional logics. For these, we obtain fully internalised calculi which are substantially simpler than those known in the literature, along with leaner proofs of cut elimination and complexity. In one case, conditional logic with modus ponens and conditional excluded middle, cut elimination and complexity were explicitly stated as open in the literature.

cs.LO↗

arXiv2009

Strong Completeness of Coalgebraic Modal Logics

Canonical models are of central importance in modal logic, in particular as they witness strong completeness and hence compactness. While the canonical model construction is well understood for Kripke semantics, non-normal modal logics often present subtle difficulties - up to the point that canonical models may fail to exist, as is the case e.g. in most probabilistic logics. Here, we present a generic canonical model construction in the semantic framework of coalgebraic modal logic, which pinpoints coherence conditions between syntax and semantics of modal logics that guarantee strong completeness. We apply this method to reconstruct canonical model theorems that are either known or folklore, and moreover instantiate our method to obtain new strong completeness results. In particular, we prove strong completeness of graded modal logic with finite multiplicities, and of the modal logic of exact probabilities.

cs.LO↗

arXiv2008

Bootstrapping Inductive and Coinductive Types in HasCASL

We discuss the treatment of initial datatypes and final process types in the wide-spectrum language HasCASL. In particular, we present specifications that illustrate how datatypes and process types arise as bootstrapped concepts using HasCASL's type class mechanism, and we describe constructions of types of finite and infinite trees that establish the conservativity of datatype and process type declarations adhering to certain reasonable formats. The latter amounts to modifying known constructions from HOL to avoid unique choice; in categorical terminology, this means that we establish that quasitoposes with an internal natural numbers object support initial algebras and final coalgebras for a range of polynomial functors, thereby partially generalising corresponding results from topos theory. Moreover, we present similar constructions in categories of internal complete partial orders in quasitoposes.

cs.LO↗

arXiv2008

Shallow Models for Non-Iterative Modal Logics

The methods used to establish PSPACE-bounds for modal logics can roughly be grouped into two classes: syntax driven methods establish that exhaustive proof search can be performed in polynomial space whereas semantic approaches directly construct shallow models. In this paper, we follow the latter approach and establish generic PSPACE-bounds for a large and heterogeneous class of modal logics in a coalgebraic framework. In particular, no complete axiomatisation of the logic under scrutiny is needed. This does not only complement our earlier, syntactic, approach conceptually, but also covers a wide variety of new examples which are difficult to harness by purely syntactic means. Apart from re-proving known complexity bounds for a large variety of structurally different logics, we apply our method to obtain previously unknown PSPACE-bounds for Elgesem's logic of agency and for graded modal logic over reflexive frames.

cs.LO↗

arXiv2007

PSPACE Bounds for Rank-1 Modal Logics

For lack of general algorithmic methods that apply to wide classes of logics, establishing a complexity bound for a given modal logic is often a laborious task. The present work is a step towards a general theory of the complexity of modal logics. Our main result is that all rank-1 logics enjoy a shallow model property and thus are, under mild assumptions on the format of their axiomatisation, in PSPACE. This leads to a unified derivation of tight PSPACE-bounds for a number of logics including K, KD, coalition logic, graded modal logic, majority logic, and probabilistic modal logic. Our generic algorithm moreover finds tableau proofs that witness pleasant proof-theoretic properties including a weak subformula property. This generality is made possible by a coalgebraic semantics, which conveniently abstracts from the details of a given model class and thus allows covering a broad range of logics in a uniform way.

cs.LO↗

arXiv2006

Linearizability of Non-expansive Semigroup Actions on Metric Spaces

We show that a non-expansive action of a topological semigroup S on a metric space X is linearizable iff its orbits are bounded. The crucial point here is to prove that X can be extended by adding a fixed point of S, thus allowing application of a semigroup version of the Arens-Eells linearization, iff the orbits of S in X are bounded.

math.MG↗