NDLI: Model checking learning agent systems using Promela with embedded C code and abstraction

Content Provider	Springer Nature Link
Author	Kirwan, Ryan Miller, Alice Porr, Bernd
Copyright Year	2016
Abstract	As autonomous systems become more prevalent, methods for their verification will become more widely used. Model checking is a formal verification technique that can help ensure the safety of autonomous systems, but in most cases it cannot be applied by novices, or in its straight “off-the-shelf” form. In order to be more widely applicable it is crucial that more sophisticated techniques are used, and are presented in a way that is reproducible by engineers and verifiers alike. In this paper we demonstrate in detail two techniques that are used to increase the power of model checking using the model checker Spin. The first of these is the use of embedded C code within Promela specifications, in order to accurately reflect robot movement. The second is to use abstraction together with a simulation relation to allow us to verify multiple environments simultaneously. We apply these techniques to a fairly simple system in which a robot moves about a fixed circular environment and learns to avoid obstacles. The learning algorithm is inspired by the way that insects learn to avoid obstacles in response to pain signals received from their antennae. Crucially, we prove that our abstraction is sound for our example system—a step that is often omitted but is vital if formal verification is to be widely accepted as a useful and meaningful approach.
Starting Page	1027
Ending Page	1056
Page Count	30
File Format	PDF
ISSN	09345043
Journal	Formal Aspects of Computing
Volume Number	28
Issue Number	6
e-ISSN	1433299X
Language	English
Publisher	Springer London
Publisher Date	2016-06-08
Publisher Place	London
Access Restriction	Subscribed
Subject Keyword	Model checking abstraction Agent Simulation Learning Math Applications in Computer Science Theory of Computation Computational Mathematics and Numerical Analysis
Content Type	Text
Resource Type	Article
Subject	Theoretical Computer Science Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Model checking learning agent systems using Promela with embedded C code and abstraction

Model checking the observational determinism security property using PROMELA and SPIN

Using probabilistic model checking for dynamic power management

Component-wise incremental LTL model checking

Model checking action system refinements

A formal semantics of extended hierarchical state transition matrices using CSP#

Assuring property conformance of code generators via model checking

Model-checking user behaviour using interacting components

Model checking RAISE applicative specifications

Model checking learning agent systems using Promela with embedded C code and abstraction

Similar Documents

Model checking learning agent systems using Promela with embedded C code and abstraction

Model checking the observational determinism security property using PROMELA and SPIN

Using probabilistic model checking for dynamic power management

Component-wise incremental LTL model checking

Model checking action system refinements

A formal semantics of extended hierarchical state transition matrices using CSP#

Assuring property conformance of code generators via model checking

Model-checking user behaviour using interacting components

Model checking RAISE applicative specifications

Model checking learning agent systems using Promela with embedded C code and abstraction