publication . Research . 1999

Establishing qualitative properties for probabilistic lossy channel systems : an algorithmic approach

Baier, Christel; Engelen, Bettina; Roggenbach, Markus;
Open Access English
  • Published: 01 Jan 1999
  • Country: Germany
Abstract
Lossy channel systems (LCSs for short) are models for communicating systems where the subprocesses are linked via unbounded FIFO channels which might lose messages. Link protocols, such as the Alternating Bit Protocol and HDLC can be modelled with these systems. The decidability of several verification problems of LCSs has been investigated by Abdulla & Jonsson [AJ93,AJ94], e.g. they have shown that the reachability problem for LCSs is decidable while LT L model checking is not. In this paper, we consider probabilistic LCSs (which are LCSs where the transitions are augmented with appropriate probabilities) as introduced by [IN97] and show that the question of wh...
Subjects
ACM Computing Classification System: ComputingMethodologies_PATTERNRECOGNITION
free text keywords: 004 Informatik
Related Organizations
Download from
48 references, page 1 of 4

[ABJ98] P. Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly analysis of systems with unbounded, lossy FIFO channels. LNCS, 1427:305-318, 1998.

[AJ93] P. Abdulla and B. Jonsson. Verifying programs with unreliable channels. Proc. LICS'93, pages 160-170, 1993. The full version with the same title has been published in Information and Computation, 127:91-101, 1996.

[AJ94] P. Abdulla and B. Jonsson. Undecidable verification problems for programs with unreliable channels. LNCS, 820:316-327, 1994. The full version with the same title has been published in Information and Computation, 130:71-90, 1996. [OpenAIRE]

[AK95] P. Abdulla and M. Kindahl. Deddability of simulation and bisimulation between lossy channel systems and finite state systems. LNCS, 962:333-347, 1995.

[AKP97] P. Abdulla, M. Kindahl, and D. Peled. An improved search strategy for lossy channel systems. In PSTV /FORTE. Chapman-Hall, 1997.

[ASBS95] A. Aziz, V. Singhal, R. Brayton, and A. Sangiovanni-Vincentelli. It usually works: The temporallogic of stochastic systems. Proc. CAV'95, 939:155-165, 1995. [OpenAIRE]

[BBS92] J. Baeten, J. Bergstra, and S. Smolka. Axiomatizing probabilistic processes: ACP with generative probabilities (extended abstract). CONCUR'92, 630:472-485, 1992. The full version with the same title has been published in Information and Computation, 122:234- 255, 1995. [OpenAIRE]

[BCG88] M. Browne, E. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporallogic. Theoretical Computer Science, 59:115-131, 1988. [OpenAIRE]

[BdA95] A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. LNCS, 1026:499-513, 1995. [OpenAIRE]

[BH97] C. Baier and H. Hermanns. Weak bisimulation for fully probabilistic processes. LNCS, 1254:119-130, 1997.

[BK98a] C. Baier and M. Kwiatkowska. Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11:125-155, 1998. [OpenAIRE]

[BK98b] C. Baier and M. Kwiatkowska. On the verification of qualitative properties of probabilistic processes under fairness constraints. Information Processing Letters, 66(2):71-79, 1998. [OpenAIRE]

[BM98] A. Bouajjani and R. Mayr. Model checking lossy vector addition systems. 1998. To appear in Proc. STACS'99, LNCS.

[Bre68] L. Breiman. Probability. Addison-Wesley Publishing Company, 1968.

[BSW69] K. Bartlett, R. Scantlebury, and P. Wilkinson. A note on reliable full-duplex transmission over half-duplex links. Communications of the ACM, 12(5):260-261, 1969. [OpenAIRE]

48 references, page 1 of 4
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue