http://hdl.handle.net/1813/7730 2013-06-20T06:42:42Z http://hdl.handle.net/1813/33380 Title: Strong Completeness for Markovian Logics Authors: Kozen, Dexter; Mardare, Radu; Panangaden, Prakash Abstract: In this paper we present Hilbert-style axiomatizations for three logics for reasoning about continuous-space Markov processes (MPs): (i) a logic for MPs defined for probability distributions on measurable state spaces, (ii) a logic for MPs defined for sub-probability distributions and (iii) a logic defined for arbitrary distributions.These logics are not compact so one needs infinitary rules in order to obtain strong completeness results. We propose a new infinitary rule that replaces the so-called Countable Additivity Rule (CAR) currently used in the literature to address the problem of proving strong completeness for these and similar logics. Unlike the CAR, our rule has a countable set of instances; consequently it allows us to apply the Rasiowa-Sikorski lemma for establishing strong completeness. Our proof method is novel and it can be used for other logics as well. 2013-06-14T00:00:00Z http://hdl.handle.net/1813/33379 Title: Scalable Network Management with Merlin Authors: Soulé, Robert; Basu, Shrutarshi; Sirer, Emin Gün; Foster, Nate Abstract: This paper presents the Merlin network management framework. With Merlin, network administrators express functionality such as accounting, bandwidth provisioning, and traffic filtering in a high-level policy language, and use automated tools and mechanisms to implement them. The framework includes: (i) a declarative language for specifying policies, (ii) infrastructure for distributing, refining, and coordinating enforcement of policies, and (iii) a run-time monitor that inspects incoming and outgoing traffic on end hosts. We describe Merlin's policy language and enforcement infrastructure, illustrate the use of Merlin on case studies, and present experimental results demonstrating that Merlin is more efficient and scalable than equivalent implementations based on programmable switches and centralized middleboxes. Overall, Merlin simplifies the task of network administration by providing high-level abstractions and tools for specifying and enforcing rich network policies. 2013-06-13T00:00:00Z http://hdl.handle.net/1813/33330 Title: Well-Founded Coalgebras, Revisited Authors: Jeannin, Jean-Baptiste; Kozen, Dexter; Silva, Alexandra Abstract: Theoretical models of recursion schemes have been well studied under the names well-founded coalgebras, recursive coalgebras, corecursive algebras, and Elgot algebras. Much of this work focuses on conditions ensuring unique or canonical solutions, e.g. when the coalgebra is well-founded. If the coalgebra is not well-founded, then there can be multiple solutions. The standard semantics of recursive programs gives a particular solution, namely the least solution in a flat Scott domain, which may not be the desired one. We have recently proposed programming language constructs to allow the specification of alternative solutions and methods to compute them. We have implemented these new constructs as an extension of OCaml. In this paper, we prove some theoretical results characterizing well-founded coalgebras that slightly extend results of Adamek, Luecke, and Milius (2007), along with several examples for which this extension is useful. We also give several examples that are not well-founded but still have a desired solution. In each case, the function would diverge under the standard semantics of recursion, but can be specified and computed with the programming language constructs we have proposed. 2013-05-24T00:00:00Z http://hdl.handle.net/1813/33124 Title: When not all bits are equal: Incorporating "worth" into information-flow measures Authors: Alvim, Mário S.; Scedrov, Andre; Schneider, Fred B. Abstract: Approaches to quantitative information flow (QIF) traditionally have presumed that all leaks involving a given number of bits are equally harmful. The presumption is unrealistic, so a new approach to QIF is described. Here, secrets are defined in terms of fields, where derived secrets obtained by combining these fields can be assigned a different “worth” (perhaps in proportion to the harm that would result from disclosure). New measures that incorporate worth into QIF are then defined; they generalize probability of guessing, guessing entropy, and Shannon entropy. A lattice of information is derived to provide an underlying algebraic structure for an adversary’s state of knowledge in this more-general setting. 2013-04-01T00:00:00Z http://hdl.handle.net/1813/33123 Title: Reconciling Exhaustive Pattern Matching with Objects Authors: Isradisaikul, Chinawat; Myers, Andrew C. Abstract: Pattern matching, an important feature of functional languages, is in conflict with data abstraction and extensibility, which are central to object-oriented languages. Modal abstraction offers an integration of deep pattern matching and convenient iteration abstractions into an object-oriented setting; however, because of data abstraction, it is challenging for a compiler to statically verify properties such as exhaustiveness. In this work, we extend modal abstraction in the JMatch language to support static, modular reasoning about exhaustiveness and redundancy. New matching specifications allow these properties to be checked using an SMT solver. We also introduce expressive pattern-matching constructs. Our evaluation shows that these new features enable more concise code and that the performance of checking exhaustiveness and redundancy is acceptable. 2013-03-29T00:00:00Z http://hdl.handle.net/1813/31565 Title: Stone Duality for Markov Processes Authors: Kozen, Dexter; Larsen, Kim G.; Mardare, Radu; Panangaden, Prakash Abstract: We define Aumann algebras, an algebraic analog of probabilistic modal logic. An Aumann algebra consists of a Boolean algebra with operators modeling probabilistic transitions. We prove that countable Aumann algebras and countably-generated continuous-space Markov processes are dual in the sense of Stone. Our results subsume existing results on completeness of probabilistic modal logics for Markov processes. 2013-03-14T00:00:00Z http://hdl.handle.net/1813/31372 Title: Typed Kleene Algebra with Products and Iteration Theories Authors: Kozen, Dexter; Mamouras, Konstantinos Abstract: We develop a typed equational system that subsumes both iteration theories and typed Kleene algebra in a common framework. Our approach is based on cartesian categories endowed with commutative strong monads to handle nondeterminism. 2013-02-22T00:00:00Z http://hdl.handle.net/1813/30798 Title: CoCaml: Programming with Coinductive Types Authors: Jeannin, Jean-Baptiste; Kozen, Dexter; Silva, Alexandra Abstract: We present CoCaml, a functional programming language extending OCaml, which allows us to define functions on coinductive datatypes parameterized by an equation solver. We provide numerous examples that attest to the usefulness of the new programming constructs, including operations on infinite lists, infinitary lambda-terms and p-adic numbers. 2012-12-31T00:00:00Z http://hdl.handle.net/1813/30510 Title: Practical Coinduction Authors: Kozen, Dexter; Silva, Alexandra Abstract: Induction is a well-established proof principle that is taught in most undergraduate programs in mathematics and computer science. In computer science, it is used primarily to reason about inductively-defined datatypes such as finite lists, finite trees, and the natural numbers. Coinduction is the dual principle that can be used to reason about coinductive datatypes such as infinite streams or trees, but it is not as widespread or as well understood. In this paper, we illustrate through several examples the use of coinduction in informal mathematical arguments. Our aim is to promote the principle as a useful tool for the working mathematician and to bring it to a level of familiarity on par with induction. We show that coinduction is not only about bisimilarity and equality of behaviors, but also applicable to a variety of functions and relations defined on coinductive datatypes. 2012-11-11T00:00:00Z http://hdl.handle.net/1813/30471 Title: Federated Identity Management Systems: A Privacy-based Characterization Authors: Birrell, Eleanor; Schneider, Fred B. Abstract: Identity management systems store attributes associated with users and facilitate authorization on the basis of these attributes. A privacy-driven characterization of the principal design choices for identity management systems is given, and existing systems are fit into this framework. The taxonomy of design choices also can guide public policy relating to identity management, which is illustrated using the United States NSTIC initiative. 2012-10-16T00:00:00Z