English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We introduce a technique for reachability analysis of Time-Basic (TB) Petrinets, a powerful formalism for real- time systems where time constraints areexpressed as intervals, representing possible transition firing times, whosebounds are functions of marking's time description. The technique consists ofbuilding a symbolic reachability graph relying on a sort of time coverage, andovercomes the limitations of the only available analyzer for TB nets, based inturn on a time-bounded inspection of a (possibly infinite) reachability-tree.The graph construction algorithm has been automated by a tool-set, brieflydescribed in the paper together with its main functionality and analysiscapability. A running example is used throughout the paper to sketch thesymbolic graph construction. A use case describing a small real system - thatthe running example is an excerpt from - has been employed to benchmark thetechnique and the tool-set. The main outcome of this test are also presented inthe paper. Ongoing work, in the perspective of integrating with amodel-checking engine, is shortly discussed.

Reachability Analysis of Time Basic Petri Nets: a Time Coverage Approach