Graphs as Models combines the strengths of two pre-existing workshop series: GT-VMT (Graph Transformation and Visual Modelling Techniques) and GRAPHITE (Graph Inspection and Traversal Engineering), but also solicits research from other related areas, such as social network analysis.
Graphs as Models offers a plattform for exchanging new ideas and results for active researchers in these areas, and is a satellite workshop of ETAPS 2017.
Graphs are used as models in all areas of computer science: examples are state space graphs, control flow graphs, syntax graphs, UML-type models of all kinds, network layouts, social networks, dependency graphs, and so forth. Once such graphical models are constructed, they can be analysed and transformed to verify their correctness within a domain, discover new properties, or produce new equivalent and/or optimised versions.
Graphs as Models’ main focus is the exchange and collaboration of researchers from different backgrounds. The workshop serves as platform to boost inter- and transdisciplinary research and wants to serve as leeway for new ideas. Thus, besides classical research presentations, the workshop is highly geared toward numerous interactive sessions.
This is a one day workshop programmed as mixture of
This workshop seeks to attract and stimulate research on the techniques for graph analysis, inspection and transformation, on an abstract level rather than in any specific domain. Thus, the concept of a graph (in its many guises) is central; contributions should address scenarios for the use of graphs in a modelling context that potentially transcend specific settings and can be applied across domains. We welcome contributions on any of the following (non-exhaustive) list of topics:
The workshop seeks submissions of several kinds:
|09:00 - 09:15||Welcome and Opening (Timo Kehrer)|
|09:15 - 10:00||Session I|
|10:00 - 10:30||Coffee Break|
|10:30 - 12:00||Session II|
|12:00 - 14:00||Lunch Break|
|14:00 - 15:30||Session III|
|15:30 - 16:00||Coffee Break|
|16:00 - 17:30||Session IV|
Abstract: General Purpose Graphics Processors (GPUs) have been used to significantly speed up computations over the past few years. One of the areas in which GPUs have led to a significant speed-up is model checking. In model checking, state spaces, large directed graphs, are explored to verify whether desirable properties hold. GPUexplore is a GPU-based model checker that uses a hash table to efficiently keep track of already explored states. As a large number of states is discovered and stored during such an exploration, the hash table should be able to quickly handle many inserts and queries concurrently. In this paper we compare two hash tables optimised for the GPU, using Cuckoo hashing and GPUExplore hashing. We compare the performance of both hash tables using random and non-random data obtained from model checking experiments, to analyse the applicability of the two hashtables for state space exploration. We conclude that Cuckoo hashing is three times faster than GPUExplore hashing for random data, and that Cuckoo hashing is five to nine times faster for non-random data. This suggests great potential to further speed up GPUexplore in the near future.
Abstract: MapReduce is a popular programming model for data-parallel computation. In MapReduce, the reducer produces an output from a list of inputs. Due to the scheduling policy of the platform, the inputs may arrive at the reducers in a different order. The commutativity problem of reducers asks if the output of a reducer is independent of the order of its inputs. Although the problem is undecidable in general, the MapReduce programs in practice are usually used for data analytics and thus require very simple data and control flow, which shed light on solving some practical instances of the problem. Today I will talk about our current progress towards a complete solution to the commutative problem.
Biography: In 2008, Yu-Fang Chen finished his Ph.D. study at the National Taiwan University and wrote his doctoral thesis on the topic of the automation of compositional verification using automata learning algorithms. In 2009, he worked as a postdoc researcher at Uppsala University, Sweden. Since 2014, Dr. Chen works as an associate research fellow at the Institute of Information Science, Academia Sinica, Taiwan. He was an assistant research fellow at the same institute from 2009 to 2014. His current research focus includes (1) applications of formal methods in MapReduce programs and (2) synthesis and analysis models of programs/systems using machine learning.He regularly publishes at conferences such as CAV and TACAS. His paper titled "When simulation meets antichains (for checking language inclusion of NFA's)" won the best theory paper award at ETAPS 2010.
Abstract: Structural biologists produce huge amounts of data on how molecules interact in cells. For example, in 2012 5000 peer reviewed publications mentioning the protein p53 were registered on PubMed. How best to organise this data so that we can extract meaningful insights about biology is the focus of my talk. A common use of data collected by structural biologists is to parameterise models simulating aspects of cell behaviour. Modelling approaches most often used require the enumeration of all potential species in the system, for instance, approaches such as petri net or those involving differential equations. These modelling approaches often lead to the construction of systems that are too large to practically implement, as the number of potential species is astronomically large! However, biologists often describe biochemical interactions using graph patterns (For example, "this region of that protein binds that region of this protein, if and only if the first region is phosphorylated"). I will show it is possible to stochastically simulate biochemical interactions in cells using graph rewriting rules, and that this approach circumvents the requirement of the enumeration of all possible species. This approach utilises the Kappa language. I will also show that the Kappa language provides a new perspective on causality in biological systems!
Biography: Pierre Boutillier completed his PhD with Hugo Herbelin at PPS laboratory in Paris on "compiling dependent pattern matching in the Coq proof assistant". Then, still at PPS and thanks to Jean Krivine, he switched from a functional programming language describing math, to Kappa, a programming language to model biology (especially protein-protein interactions). Boutillier continues to work on Kappa during his postdoc at the Harvard Medical School.
Abstract: Bigraphs were introduced by Robin Milner as a universal mathematical model for representing the spatial configuration of physical or virtual objects, their interaction capabilities and their temporal evolution. In my previous work, I have extended the theory to "bigraphs with sharing" to allow overlapping or intersecting spaces. In the first part of the talk, I will showcase four example applications of bigraphs with sharing: a wireless communication protocol, a management framework for domestic wireless networks, a strategic location-based pervasive mixed-reality game, and BigrapER, a set of tools providing an efficient implementation of computation, simulation, and visualisation for bigraphs. The second part of the talk will focus on current research: Formal analysis of multi-purpose sensor networks, Languages for programming IoT systems, Reachability and coverability in bigraphical reactive systems.
Biography: Michele Sevegnani is a Research Fellow at the University of Glasgow, based in the School of Computing Science. He received a PhD in Computing Science from the University of Glasgow, Scotland in 2012 and an MSc in Bioinformatics jointly from the universities of Edinburgh (Scotland) and Trento (Italy) in 2008. In 2013, he was awarded a Doctoral Prize Research Fellowship by the EPSRC. He was a visiting scholar at the Department of Civil and Environmental Engineering, UC Berkeley (2013), at the University of Twente, Netherlands (2014) and at the Computer Laboratory, University of Cambridge (2016). His research lies on the boundaries between mathematics (logics, category theory, probability) and computer science (event-based systems, formal methods, process calculi). His current work focusses on the theory of bigraphs and how to use it to reason about safety, reliability and predictability of location-aware, event-based, software systems, particularly complex systems that are already deployed.
Abstract: String diagrams are a powerful and intuitive graphical syntax for terms of symmetric monoidal categories (SMCs). They find many applications in computer science and are becoming increasingly relevant in other fields such as physics and control theory. An important role in many such approaches is played by equational theories of diagrams, typically oriented and applied as rewrite rules. We establish a sound and complete interpretation for this form of rewriting in terms of double pushout (DPO) rewriting of hypergraphs, subject to a convexity condition. Non-convex rewriting in this domain is also interesting, as syntactically it corresponds to rewriting modulo a chosen separable Frobenius structure. Two further results strengthening this approach will be shown. The first is that, contrary to arbitrary hypergraph rewriting, with our setup confluence becomes decidable for terminating rewriting systems. The second is a sound and complete interpretation of commutative operators as additional Frobenius structures, which addresses the problem of non-termination of commutativity as a rewrite rule.
Biography: Fabio Zanasi is a Lecturer in Computer Science at University College London. He works in the foundations of programming language theory. His recent research focusses on compositional modelling of various families of systems, such as signal flow graphs, quantum processes and Bayesian networks, using methods from algebraic semantics and category theory.
Abstract: The state of the art in Agent-based Modelling (ABM) is to identify phenomena of interest around which toy models are developed to support different explanations. Examples include the emerge of cooperation in competitive environments, analysed by games of Repeated Prisoners Dilemma (IPD), or the dynamics of opinion formation in networks, using variations on the Voter model. The design of the models is often ad-hoc, in particular when it comes to choosing their ingredients. For IPD we might consider network structure, decision making, learning, network change. Opinion formation models could address the impact of media and external events, network structure, network change, cognitive dissonance, psychological mechanisms of influence, conviction of opinion and so on. Without a systematic analysis of the choices faced when creating models and a mechanism to compare and assess their impact, models will only be useful in answering isolated questions, making little contri- bution to a comprehensive understanding of the phenomena themselves. We propose to use techniques from software engineering and semantics to support the development and assessment of ABMs. - graph transformation, as semantic representation for agent-based models - feature diagrams, to identify ingredients under consideration and state their interdependencies - extensions of graph transformation systems, to represent model fragments expressing features
Abstract: In earlier work, we were the first to investigate the potential of using graphics processing units (GPUs) to speed up explicit-state model checking. Back then, the conclusion was clearly that this potential exists, having measured speed-ups of around 10 times, compared to state-of-the-art single-core model checking. In this talk, I will present the second version of our GPU model checker, GPUexplore. Since publication of our earlier work, we have identified and implemented several approaches to improve the performance of the model checker considerably. These include enhanced lock-less hashing of the states and improved thread synchronizations. We discuss experimental results that show the impact of both the progress in hardware in the last few years and our proposed optimisations. The new version of GPUexplore running on state-of-the-art hardware can be more than 100 times faster than a sequential implementation for large models and is on average eight times faster than the previous version of the tool running on the same hardware.
For your queries and in case of problems with this web page, please contact the workshop chairs (gam2017easychair.org).