Publication

Model checking kernel P systems

Dragomir, C.
; 
Ipate, F.
; 
Konur, Savas
; 
Lefticaru, Raluca
; 
Mierla, L.M.
Publication Date
2014
End of Embargo
Supervisor
Keywords
Kernel P systems; kP systems; Membrane computing
Rights
Peer-Reviewed
Yes
Open Access status
Accepted for publication
Institution
Department
Awarded
Embargo end date
Collections
Engineering and Digital Technology Publications
Show all metadata
Additional title
Abstract
Recent research in membrane computing examines and confirms the anticipated modelling potential of kernel P systems in several case studies. On the one hand, this computational model is destined to be an abstract archetype which advocates the unity and integrity of P systems onto a single formalism. On the other hand, this envisaged convergence is conceived at the expense of a vast set of primitives and intricate semantics, an exigent context when considering the development of simulation and verification methodologies and tools. Encouraged and guided by the success and steady progress of similar undertakings, in this paper we directly address the issue of formal verification of kernel P systems by means of model checking and unveil a software framework, kpWorkbench, which integrates a set of related tools in support of our approach. A case study that centres around the well known Subset Sum problem progressively demonstrates each stage of the proposed methodology: expressing a kP system model in recently introduced kP-Lingua; the automatic translation of this model into a Promela (Spin) specification; the assisted, interactive construction of a set of LTL properties based on natural language patterns; and finally, the formal verification of these properties against the converted model, using the Spin model checker.
URI
http://hdl.handle.net/10454/10621
Version
No full-text available in the repository
Citation
Dragomir C, Ipate F, Konur S et al (2014) Model checking kernel P systems. In: Alhazov A, Cojocaru S, Gheorghe M et al. (Eds) Membrane Computing. Lecture Notes in Computer Science. Vol 8340 . Berlin, Heidelberg: Springer: 151-172.
Link to publisher’s version
Link to published version
Link to Version of Record
https://doi.org/10.1007/978-3-642-54239-8_12
Type
Conference paper
Qualification name
Notes