皆様
ジェノヴァ大学のEugenio Moggi先生の特別集中講演のお知らせです。 どうぞふるってご参加ください。
問合せ先： 石原 哉 北陸先端科学技術大学院大学 情報科学系 e-mail: [email protected] -----------------------------------------------
* JAIST Logic Seminar Series *
* This series of lectures is held as a part of JSPS Core-to-Core Program, A. Advanced Research Networks, and EU FP7 Marie Curie Actions IRSES project CORCON. (http://www.jaist.ac.jp/logic/ja/core2core, https://corcon.net/)
Dates: Tuesday 2 August, 2016, 13:30-15:10 Thursday 4 August, 2016, 13:30-15:10 Friday 5 August, 2016, 10:50-12:30
Place: JAIST, Collaboration room 7 (I-56) (Access: http://www.jaist.ac.jp/english/location/access.html)
Speaker: Eugenio Moggi (University of Genova)
*Tuesday 2 August, 2016, 13:30-15:10*
LECTURE 1: Categories of Classes for Collection Types
ABSTRACT. Collection 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*
LECTURE 2: Hybrid System Trajectories as Partial Continuous Maps
ABSTRACT. Hybrid 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*
LECTURE 3: Models, Over-approximations and Robustness
ABSTRACT. Hybrid 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.