場所：国立情報学研究所(NII) 20階ミーティングルーム室 (2009/2010)（地図）
Yuxin Deng (Shanghai Jiao Tong University)
Characterising Probabilistic Processes Logically
In this paper we work on (bi)simulation semantics of processes that exhibit both nondeterministic and probabilistic behaviour. We propose a probabilistic extension of the modal mu-calculus and show how to derive characteristic formulae for various simulation-like preorders over finite-state processes without divergence. In addition, we show that even without the fixpoint operators this probabilistic mu-calculus can be used to characterise these behavioural relations in the sense that two states are equivalent if and only if they satisfy the same set of formulae.
(Joint work with Rob van Glabbeek)
Yuxin Deng received his B.E. (1999) and M.E. (2002) from Shanghai Jiao Tong University, China, and his Ph.D. (2005) in Computer Science from Ecole des Mines de Paris, France. He spent a year as a postdoc in the School of Computer Science and Engineering at the University of New South Wales, Australia. Since 2006, he has been an associate professor in the Computer Science Department at Shanghai Jiao Tong University.
His main research interests include probabilistic concurrency theory, semantics of programming languages, and formal verification of concurrent systems.
Keisuke Nakano(University of Electro-Communications)
Simulation-based Graph Schema for View Updatability Checking of Graph Queries
Simulation can specify a relation between nodes of two graphs.
Buneman et al. proposed a simulation-based graph schema to describe the structures and contents of edge-labeled graph data.
As the schema is also represented by an edge-labeled graph, the graph transformation can directly be applied to the schema as well as graph data. This is helpful to validate graph transformations against given graph schemas for inputs and outputs. However, the simulation-based schema has the problem that the schema cannot enforce the presence of edges in graph data. In particular, the empty graph conforms to any graph schema. In this talk, we make an improvement on the simulation-based graph schema, called VU-schema, so that it can represent both exact presence and optional presence of edges. Since VU-schema has a form to be applied the graph transformation to, it achieves a more refined validation of graph transformation.
Keisuke Nakano is an assistant professor in the University of Electro-Communications. He received his Ph.D. degree from Division of Mathematics and Mathematical Analysis, Graduate School of Science, in Kyoto University, after quitting Department of Mathematics in University of Tokyo. He worked as a post-doc researcher in Graduate School of Information Science and Technology in University of Tokyo for a project on structured-document processing for 5 years before taking the current position. His research interests include program transformation, bidirectional transformation, functional programming, programming languages, and formal languages.