Published: 23rd October 2012
DOI: 10.4204/EPTCS.99
ISSN: 2075-2180

EPTCS 99

Proceedings First Workshop on
GRAPH Inspection and Traversal Engineering
Tallinn, Estonia, 1st April 2012

Edited by: Anton Wijs, Dragan Bošnački and Stefan Edelkamp

Preface
Anton Wijs, Dragan Bošnački and Stefan Edelkamp
Invited Presentation: Graph Transformation with Time for Domain-Specific Modelling and Simulation
Juan de Lara
1
Invited Presentation: Logic Without Formulas: Automata as a Computational Notation
Pierre Wolper
2
Invited Presentation: Graphs in Bioinformatics and Social Networks
Jaak Vilo
3
A structural analysis of the A5/1 state transition graph
Andreas Beckmann, Jaroslaw Fedorowicz, Jörg Keller and Ulrich Meyer
5
A Comparison of Sequential and GPU Implementations of Iterative Methods to Compute Reachability Probabilities
Elise Cormie-Bowins
20
Graph Subsumption in Abstract State Space Exploration
Eduardo Zambon and Arend Rensink
35
Efficient Instantiation of Parameterised Boolean Equation Systems to Parity Games
Gijs Kant and Jaco van de Pol
50
Lex-Partitioning: A New Option for BDD Search
Stefan Edelkamp, Peter Kissmann and Álvaro Torralba
66

Preface

Preface
These are the proceedings of the First Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2012), which took place on April 1, 2012 in Tallinn, Estonia, as a satellite event of the 15th European Joint Conferences on Theory and Practice of Software (ETAPS 2012).

The topic of the GRAPHITE workshop is graph search in all its forms in computer science. Graph search algorithms tend to have common characteristics, such as duplicate state detection, independent of their application domain. Over the past few years, it has been shown that the scalability of such algorithms can be dramatically improved by using, e.g., external memory, by exploiting parallel architectures, such as clusters, multi-core CPUs, and graphics processing units, and by using heuristics to guide the search. The goal of this event is to gather scientists from different communities, such as model checking, artificial intelligence planning, game playing, and algorithm engineering, who do research on graph search algorithms, such that awareness of each others' work is increased.

From 29 November to 4 December 2009, the same motivation led to organising Dagstuhl Seminar 09491, entitled "Graph Search Engineering". The GRAPHITE workshop resulted from the overall success of that seminar.

We had three invited speakers:
Besides that, we also had a call for technical papers. Each contribution went through a thorough reviewing process. For this, we would like to thank the GRAPHITE 2012 program committee members:
We also thank the external referees Milan Češka and Andrea Vandin for their help.

We thank all the authors of submitted papers for their contributions, and all authors of accepted papers for the quick turnaround in producing the camera-ready copies included in this proceedings. Finally, we thank the editorial board of EPTCS, and the chairs of ETAPS 2012, Tarmo Uustalu and Keiko Nakata, for their support.


Anton Wijs
Dragan Bošnački
Stefan Edelkamp

Graph Transformation with Time for Domain-Specific Modelling and Simulation

Juan de Lara (Universidad Autónoma de Madrid)

Graph Transformation with Time for Domain-Specific Modelling and SimulationGraph transformation is being increasingly used in model-based design to express the semantics of domain specific (visual) languages. Its declarative and graphical nature makes rules intuitive, while its formal semantics enables formal reasoning about system properties. However, many application domains require an explicit handling of time to accurately represent the behaviour of a real system.
In this talk, we will analyse different ways to add time to graph transformation. First, we will take inspiration from time Petri nets, assigning each rule a firing interval. Hence, rules are given a delay, and therefore can be used to model activities that do not modify the system state when they start but only when they finish. Second, inspired by the event scheduling discrete simulation world view, we provide rules with the ability to schedule the occurrence of other rules in the future. This approach is low-level and general enough to give semantics to other timing schemes and higher-level primitives, like (stochastic) delays, timers and activities.


Logic Without Formulas: Automata as a Computational Notation

Pierre Wolper (Université de Liège)

Logic Without Formulas: Automata as a Computational NotationFinite automata can be used as a representation of sets of values taken from a surprising variety of domains, including words, temporal sequences, queues, or arithmetic. This, combined with the fact that the operations corresponding to the usual operators of first-order logic are easily computable on automata representations, turns automata into a powerful tool for implementing systems that perform logic-oriented computations on such domains. The talk illustrates this approach by presenting a series of examples taken from work on verification developed during the last 30 years.


Graphs in Bioinformatics and Social Networks

Jaak Vilo

Graphs in Bioinformatics and Social NetworksBioinformatics deals with decoding mysteries of molecular level life by analyzing various types of biological data and trying to encode our current understanding of it in computable models. Many experimentally or computationally generated types of data are naturally represented as graphs or net- works: protein-protein interactions, gene regulatory networks, metabolic or signaling pathways, or even gene-gene co-expression data cut at some specific threshold. Although these graphs are explicit, they are incomplete and contain noise, as well as they lack most of the contextual information. Thus reverse-engineering will remain a great challenge for any foreseeable future.
Graphs, as a versatile tool, can be used both for representing the current limited understanding of nature for modeling purposes, or as means to solve data analysis tasks. We have used graphs for gene set function analysis [4] and module detection [2, 5]. Much more information could be added in such analyses as only a fraction of gene-gene co-expression information is currently used in such analyses essentially averaging across rank aggregation [1]. Since we do not usually know what is the correct graph of the underlying biological network, the network reconstruction has a huge search space for identifying the most appropriate models [3].
Analogy to social networks exists, as one can argue we have now first time ever access to plan- etary scale human-human interactions through Skype, Facebook, Twitter and alike. Understanding social interactions will have the potential to enhance user experiences and offer new types of services. We will discuss computing the shortest path between a pair of vertices in a graph. Classical exact methods for this problem do not scale up to contemporary, rapidly evolving social networks with hundreds of millions of users and billions of connections. A number of approximate methods have been proposed, including several landmark-based methods that have been shown to scale up to very large graphs with acceptable accuracy. We will discuss improvements to existing landmark based shortest path estimation methods. The first improvement relates to the use of shortest-path trees and the second improvement is a new landmark selection strategy that seeks to maximize the coverage of all shortest paths by the selected landmarks [6].

References

  1. Priit Adler, Raivo Kolde, Meelis Kull, Aleksandr Tkachenko, Hedi Peterson, Jüri Reimand, and Jaak Vilo (2009): Mining for coexpression across hundreds of datasets using novel rank aggregation and visualisation methods. Genome Biology 10(R139), doi:10.1186/gb-2009-10-12-r139.
  2. Stijn van Dongen (2000): Graph Clustering by Flow Simulation. Ph.D. thesis, University of Utrecht.
  3. Marc Jung, Hedi Peterson, Lukas Chavez, Pascal Kahlem, Hans Lehrach, Jaak Vilo, and James Adjaye (2010): A Data Integration Approach to Mapping OCT4 Gene Regulatory Networks Operative in Embryonic Stem Cells and Embryonal Carcinoma Cells. PLoS ONE 5(5), p. e10709, doi:10.1371/journal.pone.0010709.
  4. Jüri Reimand, Tambet Arak, and Jaak Vilo (2011): g:Profiler - a web server for functional interpretation of gene  lists (2011 update). Nucleic Acids Research 39(suppl 2), pp. W307–W315, doi:10.1093/nar/gkr378.
  5. Jüri Reimand, Laur Tooming, Hedi Peterson, Priit Adler, and Jaak Vilo (2008): GraphWeb: mining heteroge- neous biological networks for gene modules with functional significance. Nucleic Acids Research 36(suppl 2), pp. W452–W459, doi:10.1093/nar/gkn230.
  6. Konstantin Tretyakov, Abel Armas-Cervantes, Luciano García-Bañuelos, Jaak Vilo, and Marlon Dumas (2011): Fast Fully Dynamic Landmark-based Estimation of Shortest Path Distances in Very Large Graphs. In: CIKM’11, Association for Computing Machinery (ACM), Glasgow, Scotland, UK, pp. 1785–1794, doi: /10.1145/2063576.2063834.