eighty-twenty

The work is using BSPA - CCS for BSP - “Bulk synchronous process algebra”. BSPA is bilevel - local level and global level. The programmer can address processors by number within a machine, but can also send messages between machines.

There are two kinds of comm: computation within the par step; and also message-sending for the global transfer step and synchronisation barrier.

The cost model is to expand individual expression to serial form (by expanding par into sum-of-sequence) and from there using “cost rules” to arrive at an expression representing the cost of the calculation. The clever step is the recognition of the semi-ring (?).

• how is she locating the barrier expressions? sync trees?

• future work: use the cost model to evaluate the need for parallel processing, whether it would help or not in specific circumstances

This talk was about a particular graph language used to describe concurrent systems. The work focussed on analysing the graphs to identify symmetry in their Kripke structures, so that the symmetry could be reduced, thereby making the model more tractable.

Notes:

• using Promela to construct models

• is constructing the entire Kripke structure the expensive bit?

• processes and channels are typed; processes and channels are coloured by type in the diagrams

• only need to consider static topology, because if there’s symmetry in the static case, then all instances of the symmetry will introduce the same patterns of new channels later on

• “automorphism group”?

Time Petri Nets introduce timing constraints on normal Petri Nets — not sharp constraints, intervals are given for each constraint.

• “boundedness” for TPNs undecidable
• “reachability” for bounded petri nets decidable
• SCG = ??
• region graph = ??
• untimed CTL* = ??
• reachability + time CTL model-checking is decidable (1994)
• so: talk on relation between the two models
• aim: structural translation; correctness proof — both achieved
• the translation permits use of existing efficient tools for analysing TAs, eg. uppaal

Future work: real case studies, perhaps with uppaal — and investigate expressiveness — can TAs be translated back to TPNs?

This talk focussed on the first experimental validation of the APMC tool. The tool was used to compute results that were then compared with results computed by PRISM.

The summary was: PRISM and APMC are complementary tools; one might use APMC to gain a feel for the solution spaces, then switch to the slower PRISM for a precise calculation, switching back to APMC when the model grows to a size intractable to PRISM’s engine. APMC is faster than PRISM, although it does only give an approximate result.

• PRISM models nondeterminism on average systems - state space explosion when the model grows

• APMC models large systems deterministically - can only handle fully probabilistic systems (?)

• This is the first real use of APMC - it is very new, developed in 2003.

• it’s a distributed model checker! They used >80 workstations

• similar kinds of questions to those that can be asked of prism

• notions of confidence - error intervals in the answers it gives you! Statistical answers - cool!

• they built a model with apmc and it has more than 10¹⁰⁰ states! (try doing that in prism).

• the results were good - apmc lined up with prism

• I noticed that the error bars were all the same in the result graphs, so I asked a question at the end - the answer was that apmc has as an engine parameter to control the size of the required confidence interval, and that the algorithm is quadratic in the required error bound (which I’m unsure what that means exactly but the general idea is clear).

This talk reported on exploring the use of CSP in implementing a Game Semantics model-checker. Traditional model checkers don’t give soundness, completeness or compositionality — but game semantics can.

Game semantics are a series of alternating “moves” between the player (P/player/program) and the opponent (O/opponent/environment). The CSP model for game semantics has channels Q and A for questions and answers respectively. The examples look like continuation-passing-style transformed parallel-functional expressions in codename — but in CSP, which is a slightly weird language.

Their system uses LTL over finite traces. They’ve implemented a compiler from a program to the CSP representation of the game semantics for the program. The language looks imperative and algol-like. The programs are compiled into a transition system; some of the input parameters controlling the size of the transition system are set ahead of time — in the examples shown, generally the size of the input was fixed at 2 (eg. a bubblesort with arraylen = 2, and a Queue ADT with size = 2). The transition diagrams look like Satnam’s butterfly diagrams!

Using CSP instead of regular expressions to model game semantics turns out to be a clear win in terms of performance.

They implemented an algorithm that finds the minimal model for a transition diagram, but while it drastically reduces the state count in the model, the algorithm itself is really slow — just using the straight model, without minimising it, turns out to be a more efficient use of resources.

This work explores the middle ground between strict up-front formal methods and just using model checking as a debugging tool. The former doesn’t cope well with real-world projects — changes in the implementation don’t end up getting propagated all the way back to the formal model — and the latter, while enabling round-tripping to some degree, only provides a way of reasoning about fairly weak properties of the program.

L. Lamport’s TLA is used here to analyse actual software program code. It’s really only been used to analyse algorithms (ie. small isolated program fragments) and hardware specifications before.

TLA+ is a framework based on TLA that has been extended to be able to model real programs. The temporal logic in TLA is really not the main thrust — it’s there so that the temporal logic stuff fades into the background, leaving you to get real work done.

So this project attempts to allow pulling back all the way to algorithms from real code — not just having to stop at some limited properties of the program — the idea being to give the power of full up-front formal methods with the flexibility of the “debugging” approach.

The project models the C language. The model is then used as an interpreter for the program we’re ultimately interested in. The model-checker TLC tells you which transformations on your program are meaning preserving; the user then goes through the program transforming it to successively more and more abstract high-level code. Ultimately you end up with a high-level formal model of the low-level program, about which quite interesting questions can be asked and answered within the TLA+ framework.

I didn’t make many notes on this (since it’s not really my topic) except during the question time at the end, when I caught a couple of interesting questions someone else was asking:

Q: How does it compare with homology?
A: Not well. But homology is limited too, and a hybrid approach is promising.

Comment: It seems very naïve to predict tertiary structure from secondary structure with such a simplified model - there’s a long way to go.

Q: How long were the chains you tested? How big were the errors?
A: The chains were 30 to 40 amino acids long.

Notes:

• The central dogma has information flowing in one direction only. This fits the Darwinian view of the world; if information were able to flow back from proteins to the genetic (hereditary) material, we would have a more Lamarckian system. It turns out, of course, that there is information flow in the reverse direction — promoters, operons, regulatory sequences, signalling molecules etc. — but it only seldom (never?) modifies the genetic material in a heritable way.
• Michaelis-Menten equations are used to model cooperative factors in transcription.
• “Simulate Biologists! Not Biology!!” - simulate biological reasoning. Faithful simulation of the actual biological system not required.
• “Simpathica is a modular system”
• There’s a canonical form for each described reaction system.
• An example given is glycolysis. It’s written as a composition of building blocks. The modular nature of the simulation system means you can build libraries of modules.
• It does ODEs and (maybe also) PDEs
• The experiments on artificial regulatory circuits didn’t match the simulation - lots of effects need to be taken into account, e.g. RNAP run-on, …
• Very cool “story generation” technique - ask questions about a whole bunch of variations on a model - it tells you in natural language about the results! (Also can query in natural language)

SBML is an exchange language for biochemical network models. It has various levels, each an elaboration of the previous; they are intended to complement and extend one another rather than outright replacing each other, although it seems level 2 is significantly superior to level 1.

Both levels 1 and 2 are nonspatial, although level 3, currently under development, does incorporate some spatial properties. Level 2 uses MathML! Level 2 seems like a pretty standard DSL-style evolution of level 1 — refinements in order to make the language fit the domain better, addition of more language-like properties etc etc.

The reaction networks described by SBML are made up of compartments, species and reactions. The compartments are “well-stirred volumes” (how exactly are they nonspatial?). Species have to be redefined in each compartment, even if they’re notionally the same species — this seems similar to local channel names in ambients.

At level 3, some of the planned features include model composition, spatial features, diagrams (not meaningful though — just metadata hooks for GUIs to store their hand-edited layout information), and stochastic reactions. Level 2 was limited by combinatorial explosions, since species are per-compartment unique and can’t be shared; also, no record can be made of the constitution of intermediate complexes: they’re just blobs like everything else. They aren’t even marked up to be recognisable as complexes, unless some non-standard extra-systemic convention is layered on top.

Another feature being considered for level 3 is generalised reactions, where for instance you might generalize over a species’ various phosphorylation states.

There are two planned ways of composing models at level 3: by providing intermodel reactions, or by identifying species within the interlinked models. Level 3 composed models can be flattened to level 2 monolithic models.

Notes:

• SBML can build ODE models without using the subset of the language for reaction networks.

• What units are used for measuring compartment size?

• The language supports units — compound SI units! This made me think of the occasional LTU threads (1, 2) on the topic…

• Does the SBML definition of “species” fit our “alternative” model?

• He mentioned CellML as a related system.

• The planned generalised reactions are kind-of tree transformers! They only move subunits around; wildcards and backreferences would be used to leave some parts of the species untouched.

• It looks like the libSBML interop APIs might be generated by SWIG…

• libSBML has test suites and a SBML model repository available, with over 90% of the CellML repository converted to SBML.

• The next SBML forum will be 14-15 October, 2004, following ICSB 2004.

• Apparently “continuous mathematical modelling” is an interesting related topic?

• Are PDEs spatial (compared to ODEs)?

Notes:

• The lambda switch is a standard model of a bacterial gene regulation mechanism. Lambda is a virus infecting E. coli.
• The lambda switch incorporates both positive and negative feedback, as well as many different kinds of feedback loop. Only transcriptional control was considered in this talk.
• Lambda can operate in two phases: the lysogenic and the lytic phases. In lysogeny, the lambda genome is passivated and incorporated into the host cell, being replicated by the host across generations, to be reactivated into the lytic phase in some later generation. Unprompted reactivation is very rare, and is induced artificially (“induction signal”) for experimental purposes.
• [Aside: with our “alternative model” strategy for encoding biochemical reactions, does bisimulation still compute something relevant?]
• The paper covers various implementations tricks (handshakes, timers) for encoding the various interactions of proteins — there wasn’t time to cover the techniques during the talk.
• Modularity within models is a major challenge - the implementation tricks required seemed to make the model monolithic (?)
• Accessibility of π-based modelling tools to non-computer-scientists is also very important
• A question from the end: the table in the slides listing the various states of each reagent (“states of molecular actors”) is a-priori information on the control flow in the system (is it related to the lack of ambients?). The question was: how might that table be automatically derived rather than input a-priori?