On-the-fly TCTL model checking for Time Petri Nets using state class graphs

This paper shows how to efficiently model check a subclass of TCTL properties for the TPN model, using the so called state class method. The idea is to put the TPN model under analysis in parallel with a special TPN to capture relevant time events to verify a timed property. The special TPN, we call...

Full description

Saved in:
Bibliographic Details
Main Authors: Hadjidj, R., Boucheneb, H.
Format: Conference Proceeding
Language:English
Subjects:
Automata
Clocks
Explosions
Fires
Logic
Petri nets
Real time systems
Safety
State-space methods
Timing
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by
cites
container_end_page 122
container_issue
container_start_page 111
container_title
container_volume
creator Hadjidj, R.
Boucheneb, H.
description This paper shows how to efficiently model check a subclass of TCTL properties for the TPN model, using the so called state class method. The idea is to put the TPN model under analysis in parallel with a special TPN to capture relevant time events to verify a timed property. The special TPN, we call alarm-clock, has two transitions, with special firing priorities, which can be set to fire at special moments. The verification of a timed property is based on a forward on-the-fly exploration technique, augmented with an abstraction by inclusion to further attenuate the state explosion problem. We prove the decidability of our verification technique for bounded TPN models and give some experimental results to show the effectiveness of our verification technique
doi_str_mv 10.1109/ACSD.2006.18
format conference_proceeding
fullrecord <record><control><sourceid>ieee_CHZPO</sourceid><recordid>TN_cdi_ieee_primary_1640229</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><ieee_id>1640229</ieee_id><sourcerecordid>1640229</sourcerecordid><originalsourceid>FETCH-LOGICAL-i90t-905b6bc0158726ee699e0b398925b9c9cbd6416839511099a2a64c8d9dc8ffb3</originalsourceid><addsrcrecordid>eNotjz1PwzAUAC0-JNrCxsbiP-DwbMeO31gFCoiIIjV75TgvTSBpqzgM_feogumGk046xu4lJFICPi7zzVOiAGwi3QWbKZ2lwhmbXbI5ZBaNMsbqKzaTxoBIHbgbNo_xC0Db1OGMva_3YmpJNP2Jl3lZ8OFQU89DS-G72-94cxh52Q3EP2kaO_5BU-Q_8Wzi5Cfiofcx8t3oj228ZdeN7yPd_XPBNqvnMn8VxfrlLV8WokOYBIKpbBVAGpcpS2QRCSqNDpWpMGCoaptK6zSa8yF65W0aXI11cE1T6QV7-Kt2RLQ9jt3gx9NW2hSUQv0LVHVLsw</addsrcrecordid><sourcetype>Publisher</sourcetype><iscdi>true</iscdi><recordtype>conference_proceeding</recordtype></control><display><type>conference_proceeding</type><title>On-the-fly TCTL model checking for Time Petri Nets using state class graphs</title><source>IEEE Xplore All Conference Series</source><creator>Hadjidj, R. ; Boucheneb, H.</creator><creatorcontrib>Hadjidj, R. ; Boucheneb, H.</creatorcontrib><description>This paper shows how to efficiently model check a subclass of TCTL properties for the TPN model, using the so called state class method. The idea is to put the TPN model under analysis in parallel with a special TPN to capture relevant time events to verify a timed property. The special TPN, we call alarm-clock, has two transitions, with special firing priorities, which can be set to fire at special moments. The verification of a timed property is based on a forward on-the-fly exploration technique, augmented with an abstraction by inclusion to further attenuate the state explosion problem. We prove the decidability of our verification technique for bounded TPN models and give some experimental results to show the effectiveness of our verification technique</description><identifier>ISSN: 1550-4808</identifier><identifier>ISBN: 0769525563</identifier><identifier>ISBN: 9780769525563</identifier><identifier>EISSN: 2374-8567</identifier><identifier>DOI: 10.1109/ACSD.2006.18</identifier><language>eng</language><publisher>IEEE</publisher><subject>Automata ; Clocks ; Explosions ; Fires ; Logic ; Petri nets ; Real time systems ; Safety ; State-space methods ; Timing</subject><ispartof>Sixth International Conference on Application of Concurrency to System Design (ACSD'06), 2006, p.111-122</ispartof><woscitedreferencessubscribed>false</woscitedreferencessubscribed></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><linktohtml>$$Uhttps://ieeexplore.ieee.org/document/1640229$$EHTML$$P50$$Gieee$$H</linktohtml><link.rule.ids>309,310,776,780,785,786,2051,4035,4036,27904,54533,54898,54910</link.rule.ids><linktorsrc>$$Uhttps://ieeexplore.ieee.org/document/1640229$$EView_record_in_IEEE$$FView_record_in_$$GIEEE</linktorsrc></links><search><creatorcontrib>Hadjidj, R.</creatorcontrib><creatorcontrib>Boucheneb, H.</creatorcontrib><title>On-the-fly TCTL model checking for Time Petri Nets using state class graphs</title><title>Sixth International Conference on Application of Concurrency to System Design (ACSD'06)</title><addtitle>ACSD</addtitle><description>This paper shows how to efficiently model check a subclass of TCTL properties for the TPN model, using the so called state class method. The idea is to put the TPN model under analysis in parallel with a special TPN to capture relevant time events to verify a timed property. The special TPN, we call alarm-clock, has two transitions, with special firing priorities, which can be set to fire at special moments. The verification of a timed property is based on a forward on-the-fly exploration technique, augmented with an abstraction by inclusion to further attenuate the state explosion problem. We prove the decidability of our verification technique for bounded TPN models and give some experimental results to show the effectiveness of our verification technique</description><subject>Automata</subject><subject>Clocks</subject><subject>Explosions</subject><subject>Fires</subject><subject>Logic</subject><subject>Petri nets</subject><subject>Real time systems</subject><subject>Safety</subject><subject>State-space methods</subject><subject>Timing</subject><issn>1550-4808</issn><issn>2374-8567</issn><isbn>0769525563</isbn><isbn>9780769525563</isbn><fulltext>true</fulltext><rsrctype>conference_proceeding</rsrctype><creationdate>2006</creationdate><recordtype>conference_proceeding</recordtype><sourceid>6IE</sourceid><recordid>eNotjz1PwzAUAC0-JNrCxsbiP-DwbMeO31gFCoiIIjV75TgvTSBpqzgM_feogumGk046xu4lJFICPi7zzVOiAGwi3QWbKZ2lwhmbXbI5ZBaNMsbqKzaTxoBIHbgbNo_xC0Db1OGMva_3YmpJNP2Jl3lZ8OFQU89DS-G72-94cxh52Q3EP2kaO_5BU-Q_8Wzi5Cfiofcx8t3oj228ZdeN7yPd_XPBNqvnMn8VxfrlLV8WokOYBIKpbBVAGpcpS2QRCSqNDpWpMGCoaptK6zSa8yF65W0aXI11cE1T6QV7-Kt2RLQ9jt3gx9NW2hSUQv0LVHVLsw</recordid><startdate>2006</startdate><enddate>2006</enddate><creator>Hadjidj, R.</creator><creator>Boucheneb, H.</creator><general>IEEE</general><scope>6IE</scope><scope>6IL</scope><scope>CBEJK</scope><scope>RIE</scope><scope>RIL</scope></search><sort><creationdate>2006</creationdate><title>On-the-fly TCTL model checking for Time Petri Nets using state class graphs</title><author>Hadjidj, R. ; Boucheneb, H.</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-i90t-905b6bc0158726ee699e0b398925b9c9cbd6416839511099a2a64c8d9dc8ffb3</frbrgroupid><rsrctype>conference_proceedings</rsrctype><prefilter>conference_proceedings</prefilter><language>eng</language><creationdate>2006</creationdate><topic>Automata</topic><topic>Clocks</topic><topic>Explosions</topic><topic>Fires</topic><topic>Logic</topic><topic>Petri nets</topic><topic>Real time systems</topic><topic>Safety</topic><topic>State-space methods</topic><topic>Timing</topic><toplevel>online_resources</toplevel><creatorcontrib>Hadjidj, R.</creatorcontrib><creatorcontrib>Boucheneb, H.</creatorcontrib><collection>IEEE Electronic Library (IEL) Conference Proceedings</collection><collection>IEEE Proceedings Order Plan All Online (POP All Online) 1998-present by volume</collection><collection>IEEE Xplore All Conference Proceedings</collection><collection>IEEE Electronic Library (IEL)</collection><collection>IEEE Proceedings Order Plans (POP All) 1998-Present</collection></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext_linktorsrc</fulltext></delivery><addata><au>Hadjidj, R.</au><au>Boucheneb, H.</au><format>book</format><genre>proceeding</genre><ristype>CONF</ristype><atitle>On-the-fly TCTL model checking for Time Petri Nets using state class graphs</atitle><btitle>Sixth International Conference on Application of Concurrency to System Design (ACSD'06)</btitle><stitle>ACSD</stitle><date>2006</date><risdate>2006</risdate><spage>111</spage><epage>122</epage><pages>111-122</pages><issn>1550-4808</issn><eissn>2374-8567</eissn><isbn>0769525563</isbn><isbn>9780769525563</isbn><abstract>This paper shows how to efficiently model check a subclass of TCTL properties for the TPN model, using the so called state class method. The idea is to put the TPN model under analysis in parallel with a special TPN to capture relevant time events to verify a timed property. The special TPN, we call alarm-clock, has two transitions, with special firing priorities, which can be set to fire at special moments. The verification of a timed property is based on a forward on-the-fly exploration technique, augmented with an abstraction by inclusion to further attenuate the state explosion problem. We prove the decidability of our verification technique for bounded TPN models and give some experimental results to show the effectiveness of our verification technique</abstract><pub>IEEE</pub><doi>10.1109/ACSD.2006.18</doi><tpages>12</tpages></addata></record>
fulltext fulltext_linktorsrc
identifier ISSN: 1550-4808
ispartof Sixth International Conference on Application of Concurrency to System Design (ACSD'06), 2006, p.111-122
issn 1550-4808
2374-8567
language eng
recordid cdi_ieee_primary_1640229
source IEEE Xplore All Conference Series
subjects Automata
Clocks
Explosions
Fires
Logic
Petri nets
Real time systems
Safety
State-space methods
Timing
title On-the-fly TCTL model checking for Time Petri Nets using state class graphs
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2025-01-24T11%3A06%3A38IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-ieee_CHZPO&rft_val_fmt=info:ofi/fmt:kev:mtx:book&rft.genre=proceeding&rft.atitle=On-the-fly%20TCTL%20model%20checking%20for%20Time%20Petri%20Nets%20using%20state%20class%20graphs&rft.btitle=Sixth%20International%20Conference%20on%20Application%20of%20Concurrency%20to%20System%20Design%20(ACSD'06)&rft.au=Hadjidj,%20R.&rft.date=2006&rft.spage=111&rft.epage=122&rft.pages=111-122&rft.issn=1550-4808&rft.eissn=2374-8567&rft.isbn=0769525563&rft.isbn_list=9780769525563&rft_id=info:doi/10.1109/ACSD.2006.18&rft_dat=%3Cieee_CHZPO%3E1640229%3C/ieee_CHZPO%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-i90t-905b6bc0158726ee699e0b398925b9c9cbd6416839511099a2a64c8d9dc8ffb3%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_id=info:pmid/&rft_ieee_id=1640229&rfr_iscdi=true