This HTML5 document contains 36 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
n9doi:10.1007/
dctermshttp://purl.org/dc/terms/
n2https://kar.kent.ac.uk/id/eprint/
n11https://kar.kent.ac.uk/74012/
wdrshttp://www.w3.org/2007/05/powder-s#
dchttp://purl.org/dc/elements/1.1/
n4http://purl.org/ontology/bibo/status/
n19https://kar.kent.ac.uk/id/subject/
rdfshttp://www.w3.org/2000/01/rdf-schema#
n18https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/
n6http://eprints.org/ontology/
n20https://kar.kent.ac.uk/id/event/
bibohttp://purl.org/ontology/bibo/
n21https://kar.kent.ac.uk/id/org/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
n7https://kar.kent.ac.uk/id/document/
n12https://kar.kent.ac.uk/id/
n17https://kar.kent.ac.uk/id/eprint/74012#
xsdhhttp://www.w3.org/2001/XMLSchema#
n15https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/
n13https://kar.kent.ac.uk/id/person/

Statements

Subject Item
n2:74012
rdf:type
bibo:Article bibo:AcademicArticle n6:ConferenceItemEPrint n6:EPrint
rdfs:seeAlso
n11:
owl:sameAs
n9:978-3-030-25540-4_6
n6:hasAccepted
n7:3180473
n6:hasDocument
n7:3177391 n7:3177405 n7:3177406 n7:3180473 n7:3177407 n7:3180486 n7:3177408 n7:3180487 n7:3177409 n7:3180488 n7:3180489 n7:3180490
n6:hasSupplemental
n7:3177391
dc:hasVersion
n7:3180473
dcterms:title
Verifying Asynchronous Interactions via Communicating Session Automata
wdrs:describedby
n15:export_kar_RDFN3.n3 n18:export_kar_RDFN3.n3
dcterms:date
2019-07-12
dcterms:creator
n13:ext-n.yoshida@imperial.ac.uk n13:ext-j.s.lange@kent.ac.uk
bibo:status
n4:published n4:peerReviewed
dcterms:publisher
n21:ext-1c5ddec173ca8cdfba8b274309638579
bibo:abstract
This paper proposes a sound procedure to verify properties of communicating session automata (CSA), i.e., communicating automata that include multiparty session types. We introduce a new asynchronous compatibility property for CSA, called k-multiparty compatibility (k-MC), which is a strict superset of the synchronous multiparty compatibility used in theories and tools based on session types. It is decomposed into two bounded properties: (i) a condition called k-safety which guarantees that, within the bound, all sent messages can be received and each automaton can make a move; and (ii) a condition called k-exhaustivity which guarantees that all k-reachable send actions can be fired within the bound. We show that k-exhaustivity implies existential boundedness, and soundly and completely characterises systems where each automaton behaves equivalently under bounds greater than or equal to k. We show that checking k-MC is PSPACE-complete, and demonstrate its performance empirically over large systems using partial order reduction.
dcterms:isPartOf
n12:repository
dcterms:subject
n19:QA76
bibo:authorList
n17:authors
bibo:presentedAt
n20:ext-d340ceda1b1e963c421bb951f03bcc83
bibo:issue
11561