General Information

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.

Format

This is a one day workshop programmed as mixture of

• Submitted paper presentations, and
• Fully interactive sesssions, including panel discussions, brainstorm groups and informal tool demos.

Topics

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 use of graph-based and graph-transformation-based models within various general approaches such as:
  • visual modelling languages (including aspects of meta modelling, grammars, and graphical parsing),
  • model-to-model and model-to-X transformations,
  • stochastic processes on graphs, and
  • compositional models (e.g. graphs-with-boundary, nominal graphs, string diagrams),
  and applications to concrete domains, including (but not restricted to):
  • software development (e.g., synthesis, planning, bug mitigation, repair & model driven development),
  • software analysis (e.g., verification, testing, static analysis, and simulation),
  • concurrency,
  • constraint based reasoning, and
  • social network analysis;
• Algorithms on graphs (with focus on scalability and efficiency), for example
  • graph search optimization (including search space reduction techniques),
  • analysis of large graphs and graph transformation systems,
  • graph matching, isomorphism checking, etc.,
  • graph properties that support efficient algorithms regarding quality properties (like real-time, safety, reliability, and energy consumption),
  • approaches exploiting concurrency/parallelism and dedicated hardware, and
  • simulation of models.
• The visualization of large graphs (including the simulation of transformation systems).
• New ways of applying graphs and graph transformation based techniques.
• Case studies and tools.

Submissions

The workshop seeks submissions of several kinds:

• Full papers. We solicit papers of up to 15 pages, in the EPTCS LaTeX format, containing original results. Accepted papers will be published in EPTCS.
• Work-in-progress papers. We solicit papers of up to 15 pages, in the EPTCS LaTeX format, describing ongoing research. Accepted papers will be presented at the workshop and might be selected for publication in EPTCS.
• Presentation abstracts. We solicit an abstract of 1-2 pages, in the EPTCS LaTeX format, describing ongoing research. Accepted abstracts will lead to a presentation at the workshop and will be included in workshop's webpages. Submission will be accepted up to the early bird registration date.
• Informal tool demo proposals. Tool demos are limited to 10 minutes. Proposals will not be reviewed, unless selection turns out to be necessary. We solicit a 1–2 page abstract of the tool demonstration in the ETPCS LaTeX format. Submission will be accepted up to the early bird registration date.

All contributions shall be submitted through EasyChair, and adhere to EPTCS style format (available here http://style.eptcs.org). Authors of selected papers will be invited to submit an extended version of their paper to a special issue in the Elsevier journal on Science of Computer Programming (SCP) after the workshop.

Abstract/Paper/Demo Submission (extended)

February 23, 2017
(Anywhere on Earth)
Note that abstracts and Tool demos will be accepted up until the early bid registration date.

Author Notification

March 10, 2017

Final Version Due

April 7, 2017

Workshop

April 23, 2017

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 Prisoner’s 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.

Workshop Chairs

• Timo Kehrer, Politecnico di Milano
• Alice Miller, University of Glasgow

Steering Commitee Members

• Stefan Edelkamp, University of Bremen
• Frank Hermann, Carmeq GmbH
• Barbara König, University of Duisburg-Essen
• Juan de Lara, University of Madrid
• Arend Rensink, University of Twente
• Anton Wijs, University of Eindhoven

PC Members

• Luciano Baresi, Politecnico di Milano
• Paolo Bottoni, Sapienza University Rome
• Dimitrios Christopoulos, Modul University Vienna
• Andrea Corradini, University of Pisa
• Stefan Edelkamp, University of Bremen
• Andrew Fish, University of Brighton
• Reiko Heckel, University of Leicester
• Keijo Heljanko, Aalto University
• Barbara König, University of Essen-Duisburg
• Christian Krause, SAP Innovation Center Potsdam
• Leen Lambers, Hasso-Plattner-Institut, Universität Potsdam
• Renaud Lambiotte, University of Namur
• Yngve Lamo, University of Bergen
• Frédéric Lang, INRIA Grenoble Rhône-Alpes
• Juan de Lara, Universidad Autonoma de Madrid
• Mieke Massink, CNR-ISTI Pisa
• Ugo Montanari, University of Pisa
• Gethin Norman, University of Glasgow
• Julia Padberg, HAW Hamburg
• Detlef Plump, University of York
• Arend Rensink, University of Twente
• Leila Ribeiro, Universidade Federal do Rio Grande do Sul
• Andy Schürr, TU Darmstadt
• Scott Smolka, Stony Brook University
• Daniel Strüber, University of Koblenz and Landau
• Bernhard Westfechtel, University of Bayreuth
• Anton Wijs, University of Eindhoven
• Tim Willemse, Eindhoven University of Technology

ETAPS 2015 - London

the first Graphs as Models workshop. For more information, please click here

ETAPS 2016 - Eindhoven

the second Graphs as Models workshop. For more information, please click here