-
Daml: A Smart Contract Language for Securely Automating Real-World Multi-Party Business Workflows
Authors:
Alexander Bernauer,
Sofia Faro,
Rémy Hämmerle,
Martin Huschenbett,
Moritz Kiefer,
Andreas Lochbihler,
Jussi Mäki,
Francesco Mazzoli,
Simon Meier,
Neil Mitchell,
Ratko G. Veprek
Abstract:
Distributed ledger technologies, also known as blockchains for enterprises, promise to significantly reduce the high cost of automating multi-party business workflows. We argue that a programming language for writing such on-ledger logic should satisfy three desiderata: (1) Provide concepts to capture the legal rules that govern real-world business workflows. (2) Include simple means for specifyin…
▽ More
Distributed ledger technologies, also known as blockchains for enterprises, promise to significantly reduce the high cost of automating multi-party business workflows. We argue that a programming language for writing such on-ledger logic should satisfy three desiderata: (1) Provide concepts to capture the legal rules that govern real-world business workflows. (2) Include simple means for specifying policies for access and authorization. (3) Support the composition of simple workflows into complex ones, even when the simple workflows have already been deployed.
We present the open-source smart contract language Daml based on Haskell with strict evaluation. Daml achieves these desiderata by offering novel primitives for representing, accessing, and modifying data on the ledger, which are mimicking the primitives of today's legal systems. Robust access and authorization policies are specified as part of these primitives, and Daml's built-in authorization rules enable delegation, which is key for workflow composability. These properties make Daml well-suited for orchestrating business workflows across multiple, otherwise heterogeneous parties.
Daml contracts run (1) on centralized ledgers backed by a database, (2) on distributed deployments with Byzantine fault tolerant consensus, and (3) on top of conventional blockchains, as a second layer via an atomic commit protocol.
△ Less
Submitted 7 March, 2023;
originally announced March 2023.
-
The monoid of queue actions
Authors:
Martin Huschenbett,
Dietrich Kuske,
Georg Zetzsche
Abstract:
We investigate the monoid of transformations that are induced by sequences of writing to and reading from a queue storage. We describe this monoid by means of a confluent and terminating semi-Thue system and study some of its basic algebraic properties, e.g., conjugacy. Moreover, we show that while several properties concerning its rational subsets are undecidable, their uniform membership problem…
▽ More
We investigate the monoid of transformations that are induced by sequences of writing to and reading from a queue storage. We describe this monoid by means of a confluent and terminating semi-Thue system and study some of its basic algebraic properties, e.g., conjugacy. Moreover, we show that while several properties concerning its rational subsets are undecidable, their uniform membership problem is NL-complete. Furthermore, we present an algebraic characterization of this monoid's recognizable subsets. Finally, we prove that it is not Thurston-automatic.
△ Less
Submitted 22 April, 2014;
originally announced April 2014.
-
Ehrenfeucht-Fraisse Games on Omega-Terms
Authors:
Martin Huschenbett,
Manfred Kufleitner
Abstract:
Fragments of first-order logic over words can often be characterized in terms of finite monoids or finite semigroups. Usually these algebraic descriptions yield decidability of the question whether a given regular language is definable in a particular fragment. An effective algebraic characterization can be obtained from identities of so-called omega-terms. In order to show that a given fragment s…
▽ More
Fragments of first-order logic over words can often be characterized in terms of finite monoids or finite semigroups. Usually these algebraic descriptions yield decidability of the question whether a given regular language is definable in a particular fragment. An effective algebraic characterization can be obtained from identities of so-called omega-terms. In order to show that a given fragment satisfies some identity of omega-terms, one can use Ehrenfeucht-Fraisse games on word instances of the omega-terms. The resulting proofs often require a significant amount of book-kee** with respect to the constants involved. In this paper we introduce Ehrenfeucht-Fraisse games on omega-terms. To this end we assign a labeled linear order to every omega-term. Our main theorem shows that a given fragment satisfies some identity of omega-terms if and only if Duplicator has a winning strategy for the game on the resulting linear orders. This allows to avoid the book-kee**. As an application of our main result, we show that one can decide in exponential time whether all aperiodic monoids satisfy some given identity of omega-terms, thereby improving a result of McCammond (Int. J. Algebra Comput., 2001).
△ Less
Submitted 11 October, 2013;
originally announced October 2013.
-
The Rank of Tree-Automatic Linear Orderings
Authors:
Martin Huschenbett
Abstract:
We generalise Delhommé's result that each tree-automatic ordinal is strictly below ω^ω^ω by showing that any tree-automatic linear ordering has FC-rank strictly below ω^ω. We further investigate a restricted form of tree-automaticity and prove that every linear ordering which admits a tree-automatic presentation of branching complexity at most k has FC-rank strictly below ω^k.
We generalise Delhommé's result that each tree-automatic ordinal is strictly below ω^ω^ω by showing that any tree-automatic linear ordering has FC-rank strictly below ω^ω. We further investigate a restricted form of tree-automaticity and prove that every linear ordering which admits a tree-automatic presentation of branching complexity at most k has FC-rank strictly below ω^k.
△ Less
Submitted 13 April, 2012;
originally announced April 2012.
-
Tree-Automatic Well-Founded Trees
Authors:
Martin Huschenbett,
Alexander Kartzow,
Jiamou Liu,
Markus Lohrey
Abstract:
We investigate tree-automatic well-founded trees. Using Delhomme's decomposition technique for tree-automatic structures, we show that the (ordinal) rank of a tree-automatic well-founded tree is strictly below omega^omega. Moreover, we make a step towards proving that the ranks of tree-automatic well-founded partial orders are bounded by omega^omega^omega: we prove this bound for what we call upw…
▽ More
We investigate tree-automatic well-founded trees. Using Delhomme's decomposition technique for tree-automatic structures, we show that the (ordinal) rank of a tree-automatic well-founded tree is strictly below omega^omega. Moreover, we make a step towards proving that the ranks of tree-automatic well-founded partial orders are bounded by omega^omega^omega: we prove this bound for what we call upwards linear partial orders. As an application of our result, we show that the isomorphism problem for tree-automatic well-founded trees is complete for level Delta^0_{omega^omega} of the hyperarithmetical hierarchy with respect to Turing-reductions.
△ Less
Submitted 24 June, 2013; v1 submitted 26 January, 2012;
originally announced January 2012.
-
Word Automaticity of Tree Automatic Scattered Linear Orderings Is Decidable
Authors:
Martin Huschenbett
Abstract:
A tree automatic structure is a structure whose domain can be encoded by a regular tree language such that each relation is recognisable by a finite automaton processing tuples of trees synchronously. Words can be regarded as specific simple trees and a structure is word automatic if it is encodable using only these trees. The question naturally arises whether a given tree automatic structure is a…
▽ More
A tree automatic structure is a structure whose domain can be encoded by a regular tree language such that each relation is recognisable by a finite automaton processing tuples of trees synchronously. Words can be regarded as specific simple trees and a structure is word automatic if it is encodable using only these trees. The question naturally arises whether a given tree automatic structure is already word automatic. We prove that this problem is decidable for tree automatic scattered linear orderings. Moreover, we show that in case of a positive answer a word automatic presentation is computable from the tree automatic presentation.
△ Less
Submitted 24 January, 2012;
originally announced January 2012.
