The JAIST Logic Seminar series will host the following seminars in August 2016.
The seminars below are held as a part of JSPS Core-to-Core Program, A. Advanced Research Networks, and EU FP7 Marie Curie Actions IRSES project CORCON.
- Tuesday 2 August, 2016, 13:30-15:10
Eugenio Moggi (University of Genova)Categories of Classes for Collection TypesCollection types have been proposed by Buneman and others (in the ’90) as a way to capture database query languages in a typed setting. In 1998 Manes introduced the notion of collection monad on the category S of sets as a suitable semantics for collection types. The canonical example of collection monad is the finite powerset monad Pf. In order to account for the algorithmic aspects of database languages, the category S is unsuitable, and should be replaced with other categories, whose arrows are maps computable by “low complexity” algorithms. We propose “realizability for DSL” (Domain Specific Languages), where the starting point is a monoid C of endomaps on a set D, instead of a combinatory algebra on D, as a way to get such categories by constructions like the category A[C] of “assemblies”. To get Pf in a systematic way we borrow ideas from AST (Algebraic Set Theory, started by Joyal and Moerdijk in the ’90), where they fix a notion of “small” map in a category of “classes”, and read “small” as “finite”.
- Thursday 4 August, 2016, 13:30-15:10
Eugenio Moggi (University of Genova)Hybrid System Trajectories as Partial Continuous MapsHybrid systems (HS) are dynamic systems that exhibit both continuous and discrete dynamic behavior: they can flow (according to a differential equation) and jump (according to a transition relation). HS can be used for modeling rigid body dynamics with impacts, and more generally Cyber-Physical Systems. HS can exhibit Zeno behaviors, that arise naturally in rigid body dynamics with impacts, but are absent from purely discrete or purely continuous systems. Dealing properly with these behaviors is a prerequisite to give sound definitions of concepts such as reachability. We propose the use of partial continuous maps (PCM) as trajectories that describe how a HS evolves over time. PCMs enable a notion of trajectory that can go beyond Zeno points.
- Friday 5 August, 2016, 10:50-12:30
Eugenio Moggi (University of Genova)Models, Over-approximations and RobustnessHybrid systems, and related formalisms, have been successfully used to model Cyber-Physical Systems. The usual definition of “reachability”, in terms of the reflexive and transitive closure of a transition relation, is unsound for Zeno systems. We propose “safe reachability”, which gives an over-approximation of the set of states that are “reachable in finite time” from a set of initial states. Moreover, mathematical models are always a simplification of the system they are meant to describe, and one must be aware of this mismatch, when using these models for system analyses. In safety analysis it is acceptable to use over-approximations of the system behavior, indeed they are the bread and butter of counterexample guided abstraction refinement (CEGAR). We propose a notion of safe (time-bounded) reachability, which is also robust wrt arbitrary small overapproximations, and argue that it is particularly appropriate for safety analysis.
- Monday 8 August, 2016, 13:30-15:10, JAIST, Collaboration room 7 (I-56)
Marco Benini (University of Insubria)Variations on the Higman’s LemmaThe Higman’s Lemma says that if A is a well-quasi-order, so is the set of finite sequences over A with the order induced by embedding. By considering the structure of the categories of well-founded quasi-orders and well-quasi-orders, another proof of the Lemma will be derived, along with a number of variants, which may be of some interest.
- Thursday 25 August, 2016, 13:30-15:10
Helmut Schwichtenberg (Ludwig-Maximilians-Universität München)Invariance axioms for realizabilityKolmogorov (1932) proposed to consider mathematical formulas as problems asking for solutions. Following this idea it seems reasonable to extend arithmetical theories by adding invariance axioms, which state that every formula is equivalent to the (internal) formula stating that it has a realizer. We sketch such a theory, which in addition allows to fine-tune the computational content of proofs by decorations of the logical connectives. A soundness theorem holds.