In this session we present recent work in Delta Modeling. Delta Modeling is an approach towards modeling variability in software product lines. We will present the Delta Modeling Workflow (DMW), a formal step-by-step guide towards building a software product line from scratch. An approach that enjoys several beneficial properties. For …
read moreCoalgebraic Modal Logic, an Introduction
Modal logics are applied in diverse areas to reason about properties of systems. In computer science, some of the best known examples include Hennessy-Milner logic, temporal logic, and the modal mu-calculus.
Coalgebraic modal logic is a general framework for studying modal logics for systems viewed as coalgebras. In particular, basic …
read moreExamples of the Interplay between Algebra and Coalgebra
In this talk I will present in an elementary manner what is the algebra of terms for a given signature (a so called syntax), and show the interplay between such an algebra and a coalgebra, reflecting the relationship between syntax and semantics.
read moreDeterminization constructions: from automata to coalgebras
The powerset construction is a standard method for converting a nondeterministic automaton into an equivalent deterministic one as far as language is concerned. In this talk, we lift the powerset construction on automata to the more general framework of coalgebras with structured state spaces. Examples of applications include partial Mealy …
read moreCircular Behavioral Reasoning
Circular coinduction was introduced by G. Rosu and J. Goguen (IJCAR 2001, WADT 2002) as an algorithm for proving behavioral properties expressed as indistinguishability under experiments, where the experiments are described as particular contexts. Later, G. Rosu and D. Lucanu formalized the circular coinduction as a proof system (CALCO 2009 …
read moreOptimal Coin Flipping
In this talk I will show how to simulate a coin of arbitrary real bias q with a coin of arbitrary real bias p with negligible loss of entropy. I will develop a coalgebraic model and use it to derive an information-theoretic lower bound that is strictly larger than the …
read moreMeasuring Progress of Probabilistic Model-Checkers
Franck van Breugel is a professor at the Department of Computer Science and Engineering of York University, which is located in Toronto, Canada. He founded and leads the DisCoVeri group whose members carry out research in the areas of distributed computing, Verification of the source code of a probabilistic system …
read moreThe Coinductive Stream Calculus
We will consider coalgebras of the type $F(X) = mathbb{R} imes X$, representing streams over real numbers. For such streams, we coinductively define a number of operators (including, but not limited to, addition and multiplication), and we furthermore consider coinductive proofs through bisimulation. We will discuss polynomial and rational …
read moreAutomatic Verification of Real-Time Systems with Rich Data
We discuss how properties of reactive systems with continuous real-time constraints and complex, possibly infinite data can be automatically verified, exploiting recent advances in semantics, constraint-based model checking, and decision procedures for complex data.
The systems are specified in CSP-OZ-DC, a language that integrates concepts from Communicating Sequential Processes (CSP …
read moreThe Coalgebraic Approach
We shall discuss the main constituents of the coalgebraic approach to the modelling of dynamical systems and infinite data structures.
(i) A system is modelled by a map s: S -> F(S), where S is the set of the states of the system; F(-) is the system's type (formally a …
read more