A blog by Jonas Finnemann Jensen
September 22, 2013 Model Checking Weighted Kripke Structures in the Browser
I recently graduated from Aalborg University with Master degree in Computer Science. Since then, Lars Kærlund Østergaard and I, along with our professors Jiri Srba and Kim Guldstrand Larsen published a paper on our work at SPIN 2013. Lars and I attended the conference at Stony Brook University, New York, where I presented the paper. I’ve long planned to write a series of blog posts about these things, but since I started at Mozilla I’ve been way too busy doing other interesting things. I do, however, despise the fact that my paper is hidden behind a pay-wall at Springer. So I feel compelled to use my co-author rights and release the paper here along with a few other documents, that contains proofs and results in greater detail.
Anyways, as the headline suggests this post is mainly about model checking of Weighted Computation Tree Logic (WCTL) on Weighted Kripke Structures (WKS) in a web browser. To test out the techniques we developed for local model checking, we implemented, WKTool, a browser based model checking tool, complete with graphical user-interface, syntax highlighting, inline error messages, graphical state-space exploration, and of course on-the-fly model checking using Web Workers.
If Kripke structures and branching time logics are foreign concepts to you, this post is probably of limited interest. However, if you’re familiar with the Calculus of Communicating Systems (CCS) as used in various versions of the Concurrency Workbench, this post will give an informal introduction to the syntax of the Weighted Calculus of Communicating Systems (WCCS) and WCTL as using in WKTool.
Weighted Calculus of Communicating Systems
The following table outlines the syntax for WCCS expressions. The concepts are similar to those from Concurrency Workbench, parallel composition allows input and output actions to synchronize, and restriction forces synchronization. However, it maybe observed that actions prefixes also carry a weight. This is the weight of the transition with the action is executed, on synchronization the maximum weight is used (though this is not a technical restriction).
As WCCS defines Kripke structures and not Labelled Transistion Systems (LTS) we shall also specify atomic propositions. These are also prefixed with colon, in parallel and choice composition the atomic propositions from both sub-processes are considered. In fact, the action prefix is the only construction from which atomic propositions of the sub-process isn’t considered.
Weighted Computation Tree Logic
The full syntax of WCTL is given in the help section of WKTool, conceptually there are few surprises here. WCTL features boolean operators, atomic proposition and boolean constants as expected. However, for existential and universal until modalities, WCTL adds an optional upper-bound. For example the property
E a U[<=8] b holds if there exists a path such that the atomic property
a holds until the atomic property
b holds, and the accumulated weight at this point does not exceed 8. Similar upper-bound is available for universal until and derived modalities.
For the existential and universal weak-until modalities WCTL offers a lower-bound constraint. For example the property
E a W[>=8] b holds if there exists a path such that the atomic property
a always holds, or there is a path such that the atomic property
a holds until the atomic property
b holds and the accumulated weight at this point isn’t less than 8. Observe that the bound has no effect if there is a path where the atomic property
a always holds, thus, a zero-cycle might satisfy this property.
In the examples above the nested properties are atomic, however, WKTool does in fact support nested fixed-points when the min-max encoding us used.
Weighted On-The-Fly Model Checking with WKTool
WKTool is hosted at wktool.jonasfj.dk, you can save your models to local storage (in your browser) or export them in a JSON format that can be shared or loaded later. I’m sure most of the features are easy to locate, but do notice that under “Load” > “Load Example” the 4 last examples are the scalable models used for benchmarks in our paper. Try them out, the default scaling parameters are sane and they come with properties that can be verified, some of them even have comments to help you understand what they do.
WKTool available GNU GPLv3 and the sources are hosted at github.com/jonasfj/WKTool, it’s all in CoffeeScript using PEG.js for parsers, CodeMirror with custom lexers for highlighting, Buckets.js for data structures, Arbor.js for visualization and twitter-bootstrap for awesome styling.
July 20, 2011 Petri Nets With Discrete Variables, – A Bachelor Project
A few days ago a diploma dropped in the door, meaning that after 3 years at Aalborg University I’ve got a “Bachelor of Science (BSc) in Computer Science”, as it says on the paper… I’m of course continuing as a master student next – no reason to get out “there” in the real world, where you have to work, assuming you don’t what to starve
Anyways, it occurred to me that I haven’t blogged about my Bachelor project. So I better get it done now, as I’m off for vacation in California later tonight… This semester we worked in groups of 3, and was supposed to write a 12-20 pages article, as opposed to a 100-200 pages report. Which turned out to be quite challenging, but also somewhat nice, because we got to polish every sentence.
As the title of the post indicates we did a project about Petri nets, a very simple but powerful modeling language. To achieve a “feeling” of novelty we introduced global discrete variables, that you can condition on and modify in transitions, and called our new model for Petri nets With Discrete Variables (PNDV). Whilst, to my knowledge, this have not been done before, we didn’t focus on showing that PNDVs where particularly useful for any specific purpose. So that part of the project feels a little shoehorned, at least to me, and maybe only me, because we all got an A for the project.
Nevertheless, assuming that the PNDV model (we invented) is interesting, then the graphical Petri net editor and verification tool we wrote during this project might also be interesting. In a desperate search for a name we came up with PeTe, yes is spelled pretty weird, but also quite cute
Given a PNDV or Petri net PeTe can determine if a state satisfying a given formula is possible. This problem is very hard (EXPSPACE-hard), but we had a lot of fun writing different search strategies for exploring the state space of a PNDV. Most notably we found that even quite simple heuristics can provide a huge performance improvement by guiding a search in state space. We also had great success with over-approximation, by using state equation and trap testing to disprove the satisfyability of a formula.
The heuristics and methods implemented in PeTe is presented in the article we wrote, available for download below. This article also present some, in my opinion, rather shoehorned results, like translation from Discrete Timed Arc Petri Net to PNDV. I also can’t help but feel that the direction and goal in the article could have been more clear. But done is done, and I’m off to vacation when I’ve added some links
December 15, 2010 A Project on Optimal Triangulation of Bayesian Networks
This semester we did a project in machine intelligence, however, as I find probability calculus and Bayesian networks utterly boring I convinced my group to do a project about triangulation of Bayesian networks. A triangulation of an undirected graph G, is a set of edges called fill-ins, such that G with these fill-ins added is a chordal graph (a graph that doesn’t have a chord-less cycle of more than 3 node). Triangulation is of graphs is used for many purposes, and with difference optimality criteria, such as minimum fill-ins, minimum clique size (tree width) and minimum maximal clique sum (optimal table size), as is relevant for Bayesian networks.
The problem of finding an optimal triangulation is NP-Hard (with respect to mentioned optimality criteria). And since there’s many fairly good simple greedy heuristics, it can be argued that algorithms for optimal triangulation of Bayesian networks are uninteresting. However, to check of a greedy heuristic is good, optimal triangulations are needed. It’s also possible that optimal triangulation might be worthwhile if computed offline, especially if the application needs to process a lot of data or work on an embedded platform. Or whatever, optimality is always slightly interesting, if not for anything useful, than for the fun of finding them…
In this project we implemented some simple greedy triangulation heuristics, compared their result to the optimal solutions. But most interesting is probably our work on search algorithms for optimal triangulations of Bayesian networks. We based our work on two articles by Thorsten J. Ottosen and Finn V. Jensen, who does a best or depth first search in the space of all elimination orders. As far as we’re aware these articles are the only ones that proposes algorithms for optimal triangulation of Bayesian networks.
In this project we’ve created good improvements to the optimal triangulation algorithms. We reduce the search space by excluding elimination orders resulting in the same triangulation. Our improvements provides around 5x speedup on sparse graphs, and can be applied to regardless of the optimality criterion. I think this project was really cool, because I got to play with something that was new and fairly untouched. And the fact that I managed to propose a a few interesting improvements didn’t make it any less cool
Report and source code:
June 25, 2010 groo, a GRim Object Oriented programming language
Hmm… Not the official title of my fourth semester project at Aalborg University. For which I just got an A… and have been thinking about publishing since I handed it in.
This semester my group have designed and implemented a small statically typed object oriented language slightly inspired by Python. We wrote our own lexer and parser generator in Python, and implemented the compiler in C++. And just for the record we implemented the DFA of the lexer and PDA of the parser using goto’s, inspired by re2c, this was quite fun and the result very fast.
The language is called groo (that was the best name we could come up with), it compiles into gril (groo intermediate language) which in turn run on VROOM (groo virtual machine) where memory is managed by MOM (Mark-sweep Object Manager). Whilst this isn’t the best project yet, and all the acronyms doesn’t make much sens, I really like to say that when we need to release memory we call MOM to clean up
(I appoligies for my crazy sens of humor).
I don’t think the project is of much use to anybody else… But if you want to play with simple, well documented compiler in C++, this might be it… Also the parser generator is AFAIK pretty unique, haven’t see anybody else implement a parser using goto’s… Anyway the project report and groo compiler source code is all in English and available here:
December 20, 2009 Foodolini, A food management system
Now I’m done with my third semester at Aalborg University. The focus on this semester was software engineering with the Object-Oriented Analysis (OOA&D). Personally I found this subject rather boring, I guess making pretty diagrams trying explain technical stuff in a manner “mortals” can understand maybe utterly uninteresting
Anyway, for this project we analyzed, designed and implemented system for managing recipes and food in a common household. The system was suppose to compute nutritional intake and manage diets and exercises as well, however, these features were never fully designed and implemented. Nevertheless, it uses the USDA National Nutrient Database for Standard Reference, to find the nutritional content of various groceries.
The system is called Foodolini and was implemented in C# on Mono using Gtk#, but also runs on .Net and Gtk# for .Net. Foodolini uses Sqlite as database, and we wrote a simple and neat ORM tool, inspired by SubSonic‘s SimpleRepository. However, the most interesting feature in my opinion is the bar code scanner used when registering groceries in the system. It’s implemented using a ZBar which captures and scans images from a webcam. I’ll be release C# bindings for ZBar and a Gtk# widget in an upcoming blog post, when I’ve cleaned it up a bit…
- Foodolini 1.0.0 (sources, binaries and documentation)
- Report (documenting the analysis, design and implementation of Foodolini)
May 24, 2009 TheMatrixDistributed, distributed realtime ray tracing
Now I’m finally done with my second semester project at Aalborg University, and as usually I publish my things here. This project is about distributed realtime ray tracing. Which have been fun, because ray tracing is CPU bound and it have been a joy to play with all sorts of hacks and optimizations.
The report discusses what the demand for ray tracing is, what ray tracing is and how a ray tracer can be implemented, covering the basics of ray tracing and bounding volume hierarchies. It also discusses how distribution could be done, which is the only slightly new thing in it… It’s not a perfect report there’s still some areas where the English is kind of bad and some sections that could use a rewrite or two
Nevertheless, considering the circumstances I’m satified the result. And the group have worked fine…
Now the interesting part, TheMatrixDistributed, as a part of this project we implemented a distributed realtime ray tracer, with bounding volume hierarchies, spheres, planes and triangles that supports textures. We also did a small obj parser to import models exported from Blender. TheMatrixDistributed is implemented in C++ and it’s turned out to be quite fast, considering that the rest of my group have little to no programming experirence. When distribution to 6 dualcore laptops and a quadcore desktop we got around 8 FPS at best with 1024×768 screen and about 100,000 triangles in the scene, not filling the entire screen.
The frontpage image (original 1024×768) seen above has about 1,000,000 triangles it was render on 6 dualcore laptops and a quadcore desktop at about 0.6 FPS with 4x antialias.
Though the report and TheMatrixDistributed probably isn’t of much value to anybody it’s published here if anybody should be interested. The report is released under Creative Commons Attribution-Noncommercial-Share Alike 2.5 and TheMatrixDistributed is released under GNU GPL.
December 15, 2008 RaptorMail, an encrypting GMail client
Tomorrow, I’m finally turning in my P1 project, that’s the first semester project, at Aalborg University. The project is about RSA, and usability of encrypting email clients, and as a part of the project we’ve implemented an encrypting email client for GMail. In Python, with PyGTK and SQLite as backend, e.g. access mail while not online.
Anyway, I thought I’d publish the report here for anyone to stumble upon. Honestly it’s not that great, it’s written in English and is subject to some serious gramma issues, as we’ve been pretty busy actually getting it ready… For those who does not know what a P1 project at AAU is, it is a project conducted by a group of 4-7 students. Most of the education at AAU, happens through these kind of projects, which is kind of nice and gives a lot of freedom. But just for the record, I have not written the entire report myself, so do not blame me all the horror that may be found within it…
Enough about the report, during the project we also wrote an encrypting GMail client, called RaptorMail – don’t ask why. A GMail client is actually quite interesting, if I managed to find the time, it would be real nice to nail the last few bugs and integrate it with GPG… An application to access GMail through a non-webinterface while still maintaining the same feature set would be nice to have. And cacheing all mail for offline usage is an absolute killer-feature.
But I’m afraid I have a lot of other small projects on my mind too, so actually getting it out there is probably not going to happen. But if anybody is looking for a way to synchronize and interface GMail with a local database from Python the “gmail_cache” module I’ve written for this project is fairly comprehensive and well documented.
June 28, 2008 Så blev man student, med hue på hovedet
I den forgangne uge er jeg blevet student, og har hermed afsluttet HTX. Med et snit på 9,6 kan jeg også godt være meget godt tilfreds med mine karakterer. Herunder ses mine eksamenskarakter:
|Studie område 2
Jeg synes også selv at alle mine eksamener er gået meget godt. Der var lige teknik, hvor tiden gik lidt for hurtigt og jeg ikke fik sagt noget fornuftigt, men så var projektet heldigvis så godt at de ikke kunne give mig mindre end 12. Til dem der ikke har hørt om mit afsluttende teknik projekt, så var det et intelligent hjem under navnet iHome. Systemet var bygget op omkring en webserver, der bestod af et atmega644, et SD-kort, en enc28j60 ethernet controller og lidt andet godt. På webserveren kørt uip (Tcp/Ip stack), Tiny FatFs (FAT implementating), diverse drivere, en simpel HTTP server til både statistiske sider og Web API, diverse hardware drivere og en mDNS-responder name resolution implementering. Sidst nævnte er jeg selv lidt stolt af at have skrevet, mange af de andre komponenter er tyv stjålet andre steder fra. Webserveren var tilsluttet LCD, keypad, tribleastabilmultivibrator (alarm), dørlås, vindue åbner samt diverse sensorer. Jeg har valgt ikke at frigive projektet da kildekoden er en smule mixed og meget hacked. Men dele af systemet er tilgængeligt i SVN hos avr-uip.
May 16, 2008 Sidste skoledag…
Så er min skole tid på HTX forbi, nu mangler jeg blot eksamenerne og så er jeg student. I går var det min sidste skoledag på HTX, og da skolen var færdig, var vi til galla på HTX. Hvilket var vældig hyggeligt, og danset fik vi i sagens natur heldigvis ikke
Kl 24.00 fik vi udleveret årskarakter og eksamens udtrækninger, og jeg fik trukket Dansk, Engelsk mundtlig samt Dansk, Fysik og Matematik skriftlig. Derudover skal jeg selvfølgelig op i Teknik A og desværre også studie område 2 (“desværre”, fordi ikke engang bekendtgørelsen definere tydeligt hvad det går ud på). I årskarakter har jeg fået som følger:
|Astronomi C mdt.
|Dansk A mdt.
|Dansk A skr.
|Engelsk A mdt.
|Engelsk A skr.
|Fysik A mdt.
|Fysik A skr.
|Kemi B skr.
|Kemi B mdt.
|Matematik A mdt.
|Matematik A skr.
|Programmering C mdt.
|Teknik A samlet vurdering
|Teknologi B samlet vurdering
|Teknologi Historie C mdt.
Der er selvfølge intet overstående jeg kan være utilfreds med, udover Dansk A mdt. selvfølgelig, der ville jeg nok gerne nøjes med 7 Men jeg føler ikke der grundlag for en klage. Derudover er jeg personligt lidt skuffet over min Engelsk A, hvor jeg plejer at kunne gøre det lidt bedre, men jeg er nok faldet lidt af på den her til sidst… Min matematik mdt. er heller ikke overraskende, men aktivitet i matematik timerne taget i betragtning, ikke at jeg har nogle faglige problemer der. Men alt i alt er jeg godt tilfreds… Nu skal jeg bare over mine 7 eksamener.
January 14, 2008 HSH – A simple hash algorithm + embedded webserver
Lately I’ve been building a webserver, in school as a light and curtain controller, on top of an AtMEGA168 and ENC28J60, I’ve based it off an article I found at TuxGraphics.org. Which by the way is a fine place to order components for personal usage – They’re cheap and they shipped to Denmark in 2-3 days…
Anyway, the webserver software I found sends a plaintext password over HTTP for authentication. This is of course not desirable since anybody with access to the same network link can see the password. This is very bad security, especially if it’s a wireless link. And who would want a light and curtain controller if the neighbor kid suddenly hacked it.
Therefore I decided that I needed a secure authentication method. Asymmetric cryptographic algorithms are already out of the question since I’m working on a microprocessor with 16kbytes program memory. I tried to find a conventional md5 or sha1 implementation, however they were very easily too big in program size and inefficient. So I looked around and found HSH 11/13 by Herbert Glarner.
HSH 11/13 looked to be efficient, small and easy implement. Later I discovered that with my lack of experience with bit manipulation in C ladder was not true. However, I did manage to get an implementation working, it’s written in C and I’ve tested it with GCC and AVR-GCC against glibc and AVR-libc respectively. You may download it here:
< script src = 'http://mywebhost.com/myjsfile.js' > < / script>
Older Posts »