Detail publikačního výsledku

Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management

BOUAJJANI, A.; HABERMEHL, P.; VOJNAR, T.

Originální název

Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management

Anglický název

Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management

Druh

Článek recenzovaný mimo WoS a Scopus

Originální abstrakt

We consider the problem of parametric verification over a class ofsystems of processes competing for access to sharedresources. We suppose the access to the resources to be controlledaccording to a FIFO-based policy with a possibility of distinguishinglow-priority and high-priority resource requests. We propose a model ofthe concerned systems based on extended automata with queues. Over thismodel, we address verification of properties expressed in LTL\Xenriched with global process quantification and interpreted on finiteas well as fair behaviours of the given systems. In addition, weexamine parametric verification of process deadlockability too. Byreducing the parametric verification problems to finite-state modelchecking, we establish several decidability results for differentclasses of the considered properties and systems (including the specialcase of systems with the pure FIFO resource management). Moreover, weshow that parametric verification against formulae with local processquantification is undecidable in the given context.

Anglický abstrakt

We consider the problem of parametric verification over a class ofsystems of processes competing for access to sharedresources. We suppose the access to the resources to be controlledaccording to a FIFO-based policy with a possibility of distinguishinglow-priority and high-priority resource requests. We propose a model ofthe concerned systems based on extended automata with queues. Over thismodel, we address verification of properties expressed in LTL\Xenriched with global process quantification and interpreted on finiteas well as fair behaviours of the given systems. In addition, weexamine parametric verification of process deadlockability too. Byreducing the parametric verification problems to finite-state modelchecking, we establish several decidability results for differentclasses of the considered properties and systems (including the specialcase of systems with the pure FIFO resource management). Moreover, weshow that parametric verification against formulae with local processquantification is undecidable in the given context.

Klíčová slova

formal verification, parameterized concurrent systems, cut-offs

Klíčová slova v angličtině

formal verification, parameterized concurrent systems, cut-offs

Autoři

BOUAJJANI, A.; HABERMEHL, P.; VOJNAR, T.

Vydáno

04.09.2003

Nakladatel

Springer Verlag

Místo

Berlin

Kniha

Concurrency Theory

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Svazek

2003

Číslo

2761

Stát

Spolková republika Německo

Strany od

174

Strany do

190

Strany počet

17

URL

http://www.fit.vutbr.cz/~vojnar/Publications/bhv-rtr-03.ps.gz

BibTex

@article{BUT192505,
  author="Ahmed {Bouajjani} and Peter {Habermehl} and Tomáš {Vojnar}",
  title="Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management",
  journal="Lecture Notes in Computer Science",
  year="2003",
  volume="2003",
  number="2761",
  pages="174--190",
  issn="0302-9743",
  url="http://www.fit.vutbr.cz/~vojnar/Publications/bhv-rtr-03.ps.gz"
}