Springer papers


Jane Jovanovski , Maja Siljanoska , Vladimir Carevski , Dragan Sahpaski , Petar Gjorcevski , Metodi Micev , Bojan Ilijoski and Vlado Georgiev


Abstract This paper reports on an effort to build a tool for modeling, manipulation, and analysis of concurrent systems. The tool implements the CCS process language and can build labeled transition systems in Aldebaran format from CCS expressions. Furthermore, it can be used to reduce the state space of a labeled transition system and to check whether two labeled transition systems exhibit the same behaviour, using two behavioural equivalences: strong and weak bisimulation equivalence. The tool has the functionality needed to perform modeling, specification, and verification, illustrated on one classical example in the concurrency theory: the Alternating Bit Protocol.