uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Communicating Timed Automata: The More Synchronous, the More Difficult to Verify
Uppsala University, Teknisk-naturvetenskapliga vetenskapsområdet, Mathematics and Computer Science, Department of Information Technology. Uppsala University, Teknisk-naturvetenskapliga vetenskapsområdet, Mathematics and Computer Science, Department of Information Technology, Computer Systems. Datorteknik.
Uppsala University, Teknisk-naturvetenskapliga vetenskapsområdet, Mathematics and Computer Science, Department of Information Technology. Uppsala University, Teknisk-naturvetenskapliga vetenskapsområdet, Mathematics and Computer Science, Department of Information Technology, Computer Systems. Datorteknik.
2006 (English)In: Computer Aided Verification (CAV 2006), 2006, 14- p.Conference paper, Published paper (Refereed)
Abstract [en]

We study channel systems whose behaviour (sending and receiving messages

via unbounded FIFO channels) must follow given timing constraints

specifying the execution speeds of the local components. We propose

Communicating Timed Automata (CTA) to model such systems. The goal is to

study the borderline between decidable and undecidable classes of channel

systems in the timed setting. Our technical results include: (1) CTA with

one channel without shared states in the form $(A_1,A_2, c_{1,2})$ is

equivalent to one-counter machine, implying that verification problems

such as checking state reachability and channel boundedness are decidable,

and (2) CTA with two channels without sharing states in the form

$(A_1,A_2,A_3, c_{1,2},c_{2,3})$ has the power of Turing machines. Note

that in the untimed setting, these systems are no more expressive than

finite state machines. This shows that the capability of synchronizing on

time makes it substantially more difficult to verify channel systems.

Place, publisher, year, edition, pages
2006. 14- p.
Identifiers
URN: urn:nbn:se:uu:diva-10661OAI: oai:DiVA.org:uu-10661DiVA: diva2:38429
Available from: 2007-04-18 Created: 2007-04-18

Open Access in DiVA

No full text

Other links

http://www.it.uu.se/research/publications/reports/2006-008/

Authority records BETA

Krcal, PavelYi, Wang

Search in DiVA

By author/editor
Krcal, PavelYi, Wang
By organisation
Department of Information TechnologyComputer Systems

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 391 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf