1,721,171 research outputs found
Travelling processes
No full textThis paper describes a refinement-based development method for mobile processes. Process mobility is interpreted as the assignment or communication of higher-order variables, whose values are process constants or parameterised processes, in which target variables update their values and source variables lose their values. The mathematical basis for the work is Hoare and He's Unifying Theories of Programming (UTP). In this paper, we present a set of algebraic laws and refinement laws to be used for the development of mobile systems. The correctness of these laws is ensured by the UTP semantics of mobile processes. We illustrate our theory through a simple example that can be implemented in both a centralised and a distributed way. First, we present the pi-calculus specification for both systems and demonstrate that they are observationally equivalent. Next, we show how the centralised system may be step-wisely developed into the distributed one using our proposed laws
On the Complexity of Reasoning in Kleene Algebra
No full textAbstractWe study the complexity of reasoning in Kleene algebra and *-continuous Kleene algebra in the presence of extra-equational assumptions E; that is, the complexity of deciding the validity of universal Horn formulas E→s=t, where E is a finite set of equations. We obtain various levels of complexity based on the form of the assumptions E. Our main results are as follows: for *-continuous Kleene algebra, (i) if E contains only commutativity assumptions pq=qp, the problem is Π10-complete; (ii) if E contains only monoid equations, the problem is Π20-complete; and (iii) for arbitrary equations E, the problem is Π11-complete. The last problem is the universal Horn theory of the *-continuous Kleene algebras. This resolves an open question of the author [D. Kozen, 1994, Inform. and Comput.110, 366–390]
Provably Correct Compilation for Distributed Cryptographic Applications
No full text147 pagesDeveloping secure distributed systems is difficult, and even harder when advanced cryptography must be used to achieve security goals. We present Viaduct, a compiler that transforms high-level programs into secure, efficient distributed realizations. Instead of implementing a system of communicating processes, the Viaduct programmer implements a centralized, sequential program which is automatically compiled into a secure distributed version that uses cryptography. Viaduct programs specify security policies declaratively using information-flow labels, and need not mention cryptographic primitives. Unlike prior compilers for cryptographic libraries, Viaduct is general and extensible: it can efficiently and automatically combine local computation with multiple advanced cryptographic primitives such as commitments, zero-knowledge proofs, secure multiparty computation, and fully homomorphic encryption. We develop a modular security proof for Viaduct that abstracts away from the details of cryptographic mechanisms. Our proof relies on a novel unification of simulation-based security, information-flow control, choreographic programming, and sequentialization techniques for concurrent programs. To our knowledge, this is the first security proof that simultaneously addresses subtleties essential for robust, performant applications, such as multiple cryptographic mechanisms, malicious corruption, and asynchronous communication. Our approach offers a clear path toward leveraging Universal Composability to obtain end-to-end security with fully instantiated cryptographic mechanisms
Complexity of Finitely Presented Algebras
No full textAn algebra is finitely presented if there is a finite set G of generator symbols, a finite set O of operator symbols, and a finite set of defining relations where and are well-formed terms over G and O, such that is isomorphic to the free algebra on G and O modulo the congruence induced by . The uniform word problem, the finiteness problem, the triviality problem (whether is the one element algebra), and the subalgebra membership problem (whether a given element of is contained in a finitely generated subalgebra of ) for finitely presented algebras are shown to be -complete for P. The schema satisfiability problem and schema validity problem are shown to be -complete for NP and co-NP, respectively, Finally, the problem of isomorphism of finitely presented algebras is shown to be polynomial time many-one equivalent to the problem of graph isomorphism
Improving Computer-Assisted Language Learning through Hierarchical Knowledge Structures
Full text linkA common drawback in traditional language education is that all students in the same class use the same content. Since students may have different backgrounds such as prior knowledge and learning speed, one single curriculum may not be able to accommodate every student. Unfortunately, most students cannot afford personalized language learning, since preparing personalized learning content can be very time-consuming and potentially requires a significant amount of expert labor. Recently, researchers have proposed automatic systems to assist language education, such as Computer-based Assessment Systems (CAT) and Intelligent Tutoring Systems (ITS). However, previous work usually characterizes the student's knowledge and the difficulty of learning content using numeric scores, which may not be comprehensive. To improve on this, this thesis introduces hierarchical knowledge structures to assist in multiple tasks in language education. First, this structure multidimensionally characterizes the difficulty of each learning material by its relative difficulty to other materials and models the whole corpus with a graph structure. Additionally, we can utilize the hierarchical knowledge structure to multidimensionally assess a student's prior knowledge, predict the student's future performance on a specific task, and recommend learning content that is appropriate for each student. Furthermore, the hierarchical knowledge structure enables us to build a framework to characterize existing learning curricula extracted from textbooks and online learning tools, and apply expert wisdom that we have discovered to automatically design learning curricula. The hierarchical knowledge structure reduces the cost of expert labor and potentially makes language education more affordable and more engaging
Stochastic Dynamic Logics
No full textWe present the semantics of two variants of Probabilistic Propositional DynamicLogic (PPDL). Stochastic Differential Dynamic Logic is a logic for reasoning about hybrid systems with continuous state space that may evolve in contin- uous time according to stochastic differential equations, or in discrete time ac- cording to probabilistic or Angelic nondeterminism. Stochastic Game Logic can be seen as extending PPDL with Demonic nondeterminism, or Game Logic with probabilistic nondeterminism. For both logics, we develop sound reasoning principals over the presented semantics
On Action Algebras
Full text linkAction algebras have been proposed by Pratt as an alternative to Kleene algebras. Their chief advantage over Kleene algebras is that they form a finitely-based equational variety, so the essential properties of *(iteration) are captured purely equationally. However, unlike Kleene algebras, they are not closed under the formation of matrices, which renders them inapplicable in certain constructions in automata theory and the design and analysis of algorithms.In this paper we consider a class of action algebras called action lattices. An action lattice is simply an action algebra that forms a lattice under its natural order. Action lattices combine the best features of Kleene algebras and action algebras: like action algebras, they form a finitely-based equational variety; like Kleene algebras, they are closed under the formation of matrices. Moreover, they form the largest subvariety of action algebras for which this is true. All common examples of Kleene algebras appearing in automata theory, logics of programs, relational algebra, and the design and analysis of algorithms are action lattices
Halting and Equivalence of Schemes over Recursive Theories
No full textLet S be a fixed first-order signature. In this note we consider the following decision problems. (i) Given a recursive ground theory T over S, a program scheme p over S, and input values specified by ground terms t1,...,tn, does p halt on input t1,...,tn in all models of T? (ii) Given a recursive ground theory T over S and two program schemes p and q over S, are p and q equivalent in all models of T? When T is empty, these two problems are the classical halting and equivalence problems for program schemes, respectively. We show that problem (i) is r.e.-complete and problem (ii) is Pi-0-2-complete. Both these problems remain hard for their respective complexity classes even if T is empty and S is restricted to contain only a single constant, a single unary function symbol, and a single monadic predicate. It follows from (ii) that there can exist no relatively complete deductive system for scheme equivalence
Church-Rosser Made Easy
Full text linkThe Church-Rosser theorem states that the lambda-calculus is confluent under alpha- and beta-reductions. The standard proof of this result is due to Tait and Martin-Loef. In this note, we present an alternative proof based on the notion of acceptable orderings. The technique is easily modified to give confluence of the beta-eta-calculus.National Science Foundation CCF-063502
- …
