Infinite-State High-Level MSCs: Model-Checking and Realizability
Identifieur interne : 001148 ( Istex/Corpus ); précédent : 001147; suivant : 001149Infinite-State High-Level MSCs: Model-Checking and Realizability
Auteurs : Blaise Genest ; Anca Muscholl ; Helmut Seidl ; Marc ZeitounSource :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 2002.
Abstract
Abstract: We consider three natural classes of infinite-state HMSCs: globally-cooperative, locally-cooperative and local-choice HMSCs. We show first that model-checking for globally-cooperative and locally-cooperative HMSCs has the same complexity as for the class of finite-state (bounded) HMSCs. Surprisingly, model-checking local-choice HMSCs turns out to be exponentially more efficient in space than for locally-cooperative HMSCs. We also show that locally-cooperative and local-choice HMSCs can be always implemented by communicating finite states machines, provided we allow some additional (bounded) message data. Moreover, the implementation of local-choice HMSCs is deadlock-free and of linear-size.
Url:
DOI: 10.1007/3-540-45465-9_56
Links to Exploration step
ISTEX:B7048A9F0BD4AFA566C335DBAD928A1B93EEB33DLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Infinite-State High-Level MSCs: Model-Checking and Realizability</title><author><name sortKey="Genest, Blaise" sort="Genest, Blaise" uniqKey="Genest B" first="Blaise" last="Genest">Blaise Genest</name><affiliation><mods:affiliation>LIAFA, Université Paris VII, 2, pl. Jussieu, case 7014, 75251, Paris cedex 05, France</mods:affiliation></affiliation></author><author><name sortKey="Muscholl, Anca" sort="Muscholl, Anca" uniqKey="Muscholl A" first="Anca" last="Muscholl">Anca Muscholl</name><affiliation><mods:affiliation>LIAFA, Université Paris VII, 2, pl. Jussieu, case 7014, 75251, Paris cedex 05, France</mods:affiliation></affiliation></author><author><name sortKey="Seidl, Helmut" sort="Seidl, Helmut" uniqKey="Seidl H" first="Helmut" last="Seidl">Helmut Seidl</name><affiliation><mods:affiliation>FB IV, Universität Trier, 54286, Trier, Germany</mods:affiliation></affiliation></author><author><name sortKey="Zeitoun, Marc" sort="Zeitoun, Marc" uniqKey="Zeitoun M" first="Marc" last="Zeitoun">Marc Zeitoun</name><affiliation><mods:affiliation>LIAFA, Université Paris VII, 2, pl. Jussieu, case 7014, 75251, Paris cedex 05, France</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:B7048A9F0BD4AFA566C335DBAD928A1B93EEB33D</idno><date when="2002" year="2002">2002</date><idno type="doi">10.1007/3-540-45465-9_56</idno><idno type="url">https://api.istex.fr/document/B7048A9F0BD4AFA566C335DBAD928A1B93EEB33D/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">001148</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001148</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Infinite-State High-Level MSCs: Model-Checking and Realizability</title><author><name sortKey="Genest, Blaise" sort="Genest, Blaise" uniqKey="Genest B" first="Blaise" last="Genest">Blaise Genest</name><affiliation><mods:affiliation>LIAFA, Université Paris VII, 2, pl. Jussieu, case 7014, 75251, Paris cedex 05, France</mods:affiliation></affiliation></author><author><name sortKey="Muscholl, Anca" sort="Muscholl, Anca" uniqKey="Muscholl A" first="Anca" last="Muscholl">Anca Muscholl</name><affiliation><mods:affiliation>LIAFA, Université Paris VII, 2, pl. Jussieu, case 7014, 75251, Paris cedex 05, France</mods:affiliation></affiliation></author><author><name sortKey="Seidl, Helmut" sort="Seidl, Helmut" uniqKey="Seidl H" first="Helmut" last="Seidl">Helmut Seidl</name><affiliation><mods:affiliation>FB IV, Universität Trier, 54286, Trier, Germany</mods:affiliation></affiliation></author><author><name sortKey="Zeitoun, Marc" sort="Zeitoun, Marc" uniqKey="Zeitoun M" first="Marc" last="Zeitoun">Marc Zeitoun</name><affiliation><mods:affiliation>LIAFA, Université Paris VII, 2, pl. Jussieu, case 7014, 75251, Paris cedex 05, France</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s">Lecture Notes in Computer Science</title><imprint><date>2002</date></imprint><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series><idno type="istex">B7048A9F0BD4AFA566C335DBAD928A1B93EEB33D</idno><idno type="DOI">10.1007/3-540-45465-9_56</idno><idno type="ChapterID">56</idno><idno type="ChapterID">Chap56</idno></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We consider three natural classes of infinite-state HMSCs: globally-cooperative, locally-cooperative and local-choice HMSCs. We show first that model-checking for globally-cooperative and locally-cooperative HMSCs has the same complexity as for the class of finite-state (bounded) HMSCs. Surprisingly, model-checking local-choice HMSCs turns out to be exponentially more efficient in space than for locally-cooperative HMSCs. We also show that locally-cooperative and local-choice HMSCs can be always implemented by communicating finite states machines, provided we allow some additional (bounded) message data. Moreover, the implementation of local-choice HMSCs is deadlock-free and of linear-size.</div></front></TEI><istex><corpusName>springer</corpusName><author><json:item><name>Blaise Genest</name><affiliations><json:string>LIAFA, Université Paris VII, 2, pl. Jussieu, case 7014, 75251, Paris cedex 05, France</json:string></affiliations></json:item><json:item><name>Anca Muscholl</name><affiliations><json:string>LIAFA, Université Paris VII, 2, pl. Jussieu, case 7014, 75251, Paris cedex 05, France</json:string></affiliations></json:item><json:item><name>Helmut Seidl</name><affiliations><json:string>FB IV, Universität Trier, 54286, Trier, Germany</json:string></affiliations></json:item><json:item><name>Marc Zeitoun</name><affiliations><json:string>LIAFA, Université Paris VII, 2, pl. Jussieu, case 7014, 75251, Paris cedex 05, France</json:string></affiliations></json:item></author><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: We consider three natural classes of infinite-state HMSCs: globally-cooperative, locally-cooperative and local-choice HMSCs. We show first that model-checking for globally-cooperative and locally-cooperative HMSCs has the same complexity as for the class of finite-state (bounded) HMSCs. Surprisingly, model-checking local-choice HMSCs turns out to be exponentially more efficient in space than for locally-cooperative HMSCs. We also show that locally-cooperative and local-choice HMSCs can be always implemented by communicating finite states machines, provided we allow some additional (bounded) message data. Moreover, the implementation of local-choice HMSCs is deadlock-free and of linear-size.</abstract><qualityIndicators><score>6.068</score><pdfVersion>1.3</pdfVersion><pdfPageSize>430 x 650 pts</pdfPageSize><refBibsNative>false</refBibsNative><keywordCount>0</keywordCount><abstractCharCount>709</abstractCharCount><pdfWordCount>5765</pdfWordCount><pdfCharCount>28434</pdfCharCount><pdfPageCount>12</pdfPageCount><abstractWordCount>89</abstractWordCount></qualityIndicators><title>Infinite-State High-Level MSCs: Model-Checking and Realizability</title><chapterId><json:string>56</json:string><json:string>Chap56</json:string></chapterId><refBibs><json:item><host><author></author><title>ITU-TS recommendation Z</title><publicationDate>1996</publicationDate></host></json:item><json:item><author><json:item><name>R Alur</name></json:item><json:item><name>K Etessami</name></json:item><json:item><name>M Yannakakis</name></json:item></author><host><pages><last>313</last><first>304</first></pages><author></author><title>22nd Int. Conf. on Software Engineering</title><publicationDate>2000</publicationDate></host><title>Inference of message sequence charts</title><publicationDate>2000</publicationDate></json:item><json:item><author><json:item><name>R Alur</name></json:item><json:item><name>K Etessami</name></json:item><json:item><name>M Yannakakis</name></json:item></author><host><pages><last>808</last><first>797</first></pages><author></author><title>ICALP'01</title><publicationDate>2001</publicationDate></host><title>Realizability and verification of MSC graphs</title><publicationDate>2001</publicationDate></json:item><json:item><host><pages><last>77</last><first>70</first></pages><author><json:item><name>R Alur</name></json:item><json:item><name>G,H Holzmann</name></json:item><json:item><name>D,A Peled</name></json:item></author><title>An analyzer for message sequence charts. Software Concepts and Tools</title><publicationDate>1996</publicationDate></host></json:item><json:item><author><json:item><name>R Alur</name></json:item><json:item><name>M Yannakakis</name></json:item></author><host><pages><last>129</last><first>114</first></pages><author></author><title>CONCUR'99</title><publicationDate>1999</publicationDate></host><title>Model checking of message sequence charts</title><publicationDate>1999</publicationDate></json:item><json:item><author><json:item><name>D Brand</name></json:item><json:item><name>P Zafiropulo</name></json:item></author><host><volume>30</volume><pages><last>342</last><first>323</first></pages><issue>2</issue><author></author><title>Journal of the ACM</title><publicationDate>1983</publicationDate></host><title>On communicating finite-state machines</title><publicationDate>1983</publicationDate></json:item><json:item><host><author><json:item><name>B Caillaud</name></json:item><json:item><name>P Darondeau</name></json:item><json:item><name>L Hélouët</name></json:item><json:item><name>G Lesventes</name></json:item></author><title>HMSCs as partial specifications ... with PNs as completions</title><publicationDate>2000</publicationDate></host></json:item><json:item><author><json:item><name>L Hélouët</name></json:item><json:item><name>C Jard</name></json:item></author><host><author></author><title>5th Int. Workshop on Formal Methods for Ind. Crit. Systems</title><publicationDate>2000</publicationDate></host><title>Conditions for synthesis of communicating automata from HMSCs</title><publicationDate>2000</publicationDate></json:item><json:item><author><json:item><name>L Hélouët</name></json:item><json:item><name>P. Le Maigat</name></json:item></author><host><pages><last>60</last><first>46</first></pages><author></author><title>SAM2000</title><publicationDate>2000</publicationDate></host><title>Decomposition of Message Sequence Charts</title><publicationDate>2000</publicationDate></json:item><json:item><author><json:item><name>J,G Henriksen</name></json:item><json:item><name>M Mukund</name></json:item><json:item><name>K Narayan</name></json:item><json:item><name>P Kumar</name></json:item><json:item><name> Thiagarajan</name></json:item></author><host><pages><last>686</last><first>675</first></pages><author></author><title>ICALP'00</title><publicationDate>2000</publicationDate></host><title>On message sequence graphs and finitely generated regular msc languages</title><publicationDate>2000</publicationDate></json:item><json:item><author><json:item><name>Y Métivier</name></json:item></author><host><volume>58</volume><pages><last>208</last><first>201</first></pages><author></author><title>Theoretical Computer Science</title><publicationDate>1988</publicationDate></host><title>On recognizable subsets of free partially commutative monoids</title><publicationDate>1988</publicationDate></json:item><json:item><author><json:item><name>R Morin</name></json:item></author><host><pages><last>534</last><first>523</first></pages><author></author><title>STACS'02</title><publicationDate>2002</publicationDate></host><title>Recognizable Sets of Message Sequence Charts</title><publicationDate>2002</publicationDate></json:item><json:item><author><json:item><name>M Mukund</name></json:item><json:item><name>K Narayan</name></json:item><json:item><name>M Kumar</name></json:item><json:item><name> Sohoni</name></json:item></author><host><pages><last>535</last><first>521</first></pages><author></author><title>CONCUR'00</title><publicationDate>2000</publicationDate></host><title>Synthesizing distributed finitestate systems from MSCs</title><publicationDate>2000</publicationDate></json:item><json:item><author><json:item><name>A Muscholl</name></json:item><json:item><name>D Peled</name></json:item></author><host><pages><last>91</last><first>81</first></pages><author></author><title>MFCS'99</title><publicationDate>1999</publicationDate></host><title>Message sequence graphs and decision problems on Mazurkiewicz traces</title><publicationDate>1999</publicationDate></json:item><json:item><author><json:item><name>E Ochma´ochma´nski</name></json:item></author><host><pages><last>204</last><first>167</first></pages><author></author><title>The Book of Traces, chapter 6</title><publicationDate>1995</publicationDate></host><title>Recognizable trace languages</title><publicationDate>1995</publicationDate></json:item></refBibs><genre><json:string>conference</json:string></genre><serie><editor><json:item><name>Gerhard Goos</name><affiliations><json:string>Karlsruhe University, Germany</json:string></affiliations></json:item><json:item><name>Juris Hartmanis</name><affiliations><json:string>Cornell University, NY, USA</json:string></affiliations></json:item><json:item><name>Jan van Leeuwen</name><affiliations><json:string>Utrecht University, The Netherlands</json:string></affiliations></json:item></editor><issn><json:string>0302-9743</json:string></issn><language><json:string>unknown</json:string></language><title>Lecture Notes in Computer Science</title><copyrightDate>2002</copyrightDate></serie><host><editor><json:item><name>Peter Widmayer</name><affiliations><json:string>Institute of Theoretical Computer Science, ETH Zentrum, ETH Zürich, 8092, Zürich, Switzerland</json:string><json:string>E-mail: widmayer@inf.ethz.ch</json:string></affiliations></json:item><json:item><name>Stephan Eidenbenz</name><affiliations><json:string>Institute of Theoretical Computer Science, ETH Zentrum, ETH Zürich, 8092, Zürich, Switzerland</json:string><json:string>E-mail: eidenben@inf.ethz.ch</json:string></affiliations></json:item><json:item><name>Francisco Triguero</name><affiliations><json:string>Department of Languages and Sciences of the Computation E.T.S. de Ingeniería Informática, University of Málaga, Campus de Teatinos, 29071, Málaga, Spain</json:string><json:string>E-mail: triguero@lcc.uma.es</json:string></affiliations></json:item><json:item><name>Rafael Morales</name><affiliations><json:string>Department of Languages and Sciences of the Computation E.T.S. de Ingeniería Informática, University of Málaga, Campus de Teatinos, 29071, Málaga, Spain</json:string><json:string>E-mail: morales@lcc.uma.es</json:string></affiliations></json:item><json:item><name>Ricardo Conejo</name><affiliations><json:string>Department of Languages and Sciences of the Computation E.T.S. de Ingeniería Informática, University of Málaga, Campus de Teatinos, 29071, Málaga, Spain</json:string><json:string>E-mail: conejo@lcc.uma.es</json:string></affiliations></json:item><json:item><name>Matthew Hennessy</name><affiliations><json:string>School of Cognitive and Computing Sciences, University of Sussex, BN1 9QN, Falmer, Brighton, UK</json:string><json:string>E-mail: matthewh@cogs.susx.ac.uk</json:string></affiliations></json:item></editor><subject><json:item><value>Computer Science</value></json:item><json:item><value>Computer Science</value></json:item><json:item><value>Theory of Computation</value></json:item><json:item><value>Software Engineering/Programming and Operating Systems</value></json:item><json:item><value>Mathematics of Computing</value></json:item><json:item><value>Computer Graphics</value></json:item><json:item><value>Data Structures, Cryptology and Information Theory</value></json:item></subject><isbn><json:string>978-3-540-43864-9</json:string></isbn><language><json:string>unknown</json:string></language><title>Automata, Languages and Programming</title><bookId><json:string>3-540-45465-9</json:string></bookId><volume>2380</volume><pages><last>668</last><first>657</first></pages><issn><json:string>0302-9743</json:string></issn><genre><json:string>book-series</json:string></genre><eisbn><json:string>978-3-540-45465-6</json:string></eisbn><copyrightDate>2002</copyrightDate><doi><json:string>10.1007/3-540-45465-9</json:string></doi></host><publicationDate>2002</publicationDate><copyrightDate>2002</copyrightDate><doi><json:string>10.1007/3-540-45465-9_56</json:string></doi><id>B7048A9F0BD4AFA566C335DBAD928A1B93EEB33D</id><score>0.31789735</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/document/B7048A9F0BD4AFA566C335DBAD928A1B93EEB33D/fulltext/pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/document/B7048A9F0BD4AFA566C335DBAD928A1B93EEB33D/fulltext/zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/document/B7048A9F0BD4AFA566C335DBAD928A1B93EEB33D/fulltext/tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Infinite-State High-Level MSCs: Model-Checking and Realizability</title><title level="a" type="sub" xml:lang="en">Extended Abstract</title><respStmt><resp>Références bibliographiques récupérées via GROBID</resp><name resp="ISTEX-API">ISTEX-API (INIST-CNRS)</name></respStmt><respStmt><resp>Références bibliographiques récupérées via GROBID</resp><name resp="ISTEX-API">ISTEX-API (INIST-CNRS)</name></respStmt></titleStmt><publicationStmt><authority>ISTEX</authority><publisher>Springer Berlin Heidelberg</publisher><pubPlace>Berlin, Heidelberg</pubPlace><availability><p>Springer-Verlag Berlin Heidelberg, 2002</p></availability><date>2002</date></publicationStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Infinite-State High-Level MSCs: Model-Checking and Realizability</title><title level="a" type="sub" xml:lang="en">Extended Abstract</title><author xml:id="author-1"><persName><forename type="first">Blaise</forename><surname>Genest</surname></persName><affiliation>LIAFA, Université Paris VII, 2, pl. Jussieu, case 7014, 75251, Paris cedex 05, France</affiliation></author><author xml:id="author-2"><persName><forename type="first">Anca</forename><surname>Muscholl</surname></persName><affiliation>LIAFA, Université Paris VII, 2, pl. Jussieu, case 7014, 75251, Paris cedex 05, France</affiliation></author><author xml:id="author-3"><persName><forename type="first">Helmut</forename><surname>Seidl</surname></persName><affiliation>FB IV, Universität Trier, 54286, Trier, Germany</affiliation></author><author xml:id="author-4"><persName><forename type="first">Marc</forename><surname>Zeitoun</surname></persName><affiliation>LIAFA, Université Paris VII, 2, pl. Jussieu, case 7014, 75251, Paris cedex 05, France</affiliation></author></analytic><monogr><title level="m">Automata, Languages and Programming</title><title level="m" type="sub">29th International Colloquium, ICALP 2002 Málaga, Spain, July 8–13, 2002 Proceedings</title><idno type="pISBN">978-3-540-43864-9</idno><idno type="eISBN">978-3-540-45465-6</idno><idno type="pISSN">0302-9743</idno><idno type="DOI">10.1007/3-540-45465-9</idno><idno type="book-ID">3-540-45465-9</idno><idno type="book-title-ID">72412</idno><idno type="book-sequence-number">2380</idno><idno type="book-volume-number">2380</idno><idno type="book-chapter-count">90</idno><editor><persName><forename type="first">Peter</forename><surname>Widmayer</surname></persName><email>widmayer@inf.ethz.ch</email><affiliation>Institute of Theoretical Computer Science, ETH Zentrum, ETH Zürich, 8092, Zürich, Switzerland</affiliation></editor><editor><persName><forename type="first">Stephan</forename><surname>Eidenbenz</surname></persName><email>eidenben@inf.ethz.ch</email><affiliation>Institute of Theoretical Computer Science, ETH Zentrum, ETH Zürich, 8092, Zürich, Switzerland</affiliation></editor><editor><persName><forename type="first">Francisco</forename><surname>Triguero</surname></persName><email>triguero@lcc.uma.es</email><affiliation>Department of Languages and Sciences of the Computation E.T.S. de Ingeniería Informática, University of Málaga, Campus de Teatinos, 29071, Málaga, Spain</affiliation></editor><editor><persName><forename type="first">Rafael</forename><surname>Morales</surname></persName><email>morales@lcc.uma.es</email><affiliation>Department of Languages and Sciences of the Computation E.T.S. de Ingeniería Informática, University of Málaga, Campus de Teatinos, 29071, Málaga, Spain</affiliation></editor><editor><persName><forename type="first">Ricardo</forename><surname>Conejo</surname></persName><email>conejo@lcc.uma.es</email><affiliation>Department of Languages and Sciences of the Computation E.T.S. de Ingeniería Informática, University of Málaga, Campus de Teatinos, 29071, Málaga, Spain</affiliation></editor><editor><persName><forename type="first">Matthew</forename><surname>Hennessy</surname></persName><email>matthewh@cogs.susx.ac.uk</email><affiliation>School of Cognitive and Computing Sciences, University of Sussex, BN1 9QN, Falmer, Brighton, UK</affiliation></editor><imprint><publisher>Springer Berlin Heidelberg</publisher><pubPlace>Berlin, Heidelberg</pubPlace><date type="published" when="2002-06-25"></date><biblScope unit="volume">2380</biblScope><biblScope unit="page" from="657">657</biblScope><biblScope unit="page" to="668">668</biblScope></imprint></monogr><series><title level="s">Lecture Notes in Computer Science</title><editor><persName><forename type="first">Gerhard</forename><surname>Goos</surname></persName><affiliation>Karlsruhe University, Germany</affiliation></editor><editor><persName><forename type="first">Juris</forename><surname>Hartmanis</surname></persName><affiliation>Cornell University, NY, USA</affiliation></editor><editor><persName><forename type="first">Jan</forename><surname>van Leeuwen</surname></persName><affiliation>Utrecht University, The Netherlands</affiliation></editor><biblScope><date>2002</date></biblScope><idno type="pISSN">0302-9743</idno><idno type="series-Id">558</idno></series><idno type="istex">B7048A9F0BD4AFA566C335DBAD928A1B93EEB33D</idno><idno type="DOI">10.1007/3-540-45465-9_56</idno><idno type="ChapterID">56</idno><idno type="ChapterID">Chap56</idno></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>2002</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>Abstract: We consider three natural classes of infinite-state HMSCs: globally-cooperative, locally-cooperative and local-choice HMSCs. We show first that model-checking for globally-cooperative and locally-cooperative HMSCs has the same complexity as for the class of finite-state (bounded) HMSCs. Surprisingly, model-checking local-choice HMSCs turns out to be exponentially more efficient in space than for locally-cooperative HMSCs. We also show that locally-cooperative and local-choice HMSCs can be always implemented by communicating finite states machines, provided we allow some additional (bounded) message data. Moreover, the implementation of local-choice HMSCs is deadlock-free and of linear-size.</p></abstract><textClass><keywords scheme="Book-Subject-Collection"><list><label>SUCO11645</label><item><term>Computer Science</term></item></list></keywords></textClass><textClass><keywords scheme="Book-Subject-Group"><list><label>I</label><label>I16005</label><label>I14002</label><label>I17001</label><label>I22013</label><label>I15009</label><item><term>Computer Science</term></item><item><term>Theory of Computation</term></item><item><term>Software Engineering/Programming and Operating Systems</term></item><item><term>Mathematics of Computing</term></item><item><term>Computer Graphics</term></item><item><term>Data Structures, Cryptology and Information Theory</term></item></list></keywords></textClass></profileDesc><revisionDesc><change when="2002-06-25">Published</change><change xml:id="refBibs-istex" who="#ISTEX-API" when="2016-11-22">References added</change><change xml:id="refBibs-istex" who="#ISTEX-API" when="2017-01-20">References added</change></revisionDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/document/B7048A9F0BD4AFA566C335DBAD928A1B93EEB33D/fulltext/txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="Springer, Publisher found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType><istex:document><Publisher><PublisherInfo><PublisherName>Springer Berlin Heidelberg</PublisherName><PublisherLocation>Berlin, Heidelberg</PublisherLocation></PublisherInfo><Series><SeriesInfo SeriesType="Series" TocLevels="0"><SeriesID>558</SeriesID><SeriesPrintISSN>0302-9743</SeriesPrintISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName><FamilyName>Goos</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Juris</GivenName><FamilyName>Hartmanis</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Jan</GivenName><Particle>van</Particle><FamilyName>Leeuwen</FamilyName></EditorName></Editor><Affiliation ID="Aff1"><OrgName>Karlsruhe University</OrgName><OrgAddress><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgName>Cornell University</OrgName><OrgAddress><State>NY</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff3"><OrgName>Utrecht University</OrgName><OrgAddress><Country>The Netherlands</Country></OrgAddress></Affiliation></EditorGroup></SeriesHeader><Book Language="En"><BookInfo BookProductType="Proceedings" Language="En" MediaType="eBook" NumberingStyle="Unnumbered" TocLevels="0"><BookID>3-540-45465-9</BookID><BookTitle>Automata, Languages and Programming</BookTitle><BookSubTitle>29th International Colloquium, ICALP 2002 Málaga, Spain, July 8–13, 2002 Proceedings</BookSubTitle><BookVolumeNumber>2380</BookVolumeNumber><BookSequenceNumber>2380</BookSequenceNumber><BookDOI>10.1007/3-540-45465-9</BookDOI><BookTitleID>72412</BookTitleID><BookPrintISBN>978-3-540-43864-9</BookPrintISBN><BookElectronicISBN>978-3-540-45465-6</BookElectronicISBN><BookChapterCount>90</BookChapterCount><BookHistory><OnlineDate><Year>2002</Year><Month>6</Month><Day>25</Day></OnlineDate></BookHistory><BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2002</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I16005" Priority="1" Type="Secondary">Theory of Computation</BookSubject><BookSubject Code="I14002" Priority="2" Type="Secondary">Software Engineering/Programming and Operating Systems</BookSubject><BookSubject Code="I17001" Priority="3" Type="Secondary">Mathematics of Computing</BookSubject><BookSubject Code="I22013" Priority="4" Type="Secondary">Computer Graphics</BookSubject><BookSubject Code="I15009" Priority="5" Type="Secondary">Data Structures, Cryptology and Information Theory</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup><BookContext><SeriesID>558</SeriesID></BookContext></BookInfo><BookHeader><EditorGroup><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Peter</GivenName><FamilyName>Widmayer</FamilyName></EditorName><Contact><Email>widmayer@inf.ethz.ch</Email></Contact></Editor><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Stephan</GivenName><FamilyName>Eidenbenz</FamilyName></EditorName><Contact><Email>eidenben@inf.ethz.ch</Email></Contact></Editor><Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Francisco</GivenName><FamilyName>Triguero</FamilyName></EditorName><Contact><Email>triguero@lcc.uma.es</Email></Contact></Editor><Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Rafael</GivenName><FamilyName>Morales</FamilyName></EditorName><Contact><Email>morales@lcc.uma.es</Email></Contact></Editor><Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Ricardo</GivenName><FamilyName>Conejo</FamilyName></EditorName><Contact><Email>conejo@lcc.uma.es</Email></Contact></Editor><Editor AffiliationIDS="Aff6"><EditorName DisplayOrder="Western"><GivenName>Matthew</GivenName><FamilyName>Hennessy</FamilyName></EditorName><Contact><Email>matthewh@cogs.susx.ac.uk</Email></Contact></Editor><Affiliation ID="Aff4"><OrgDivision>Institute of Theoretical Computer Science, ETH Zentrum</OrgDivision><OrgName>ETH Zürich</OrgName><OrgAddress><Postcode>8092</Postcode><City>Zürich</City><Country>Switzerland</Country></OrgAddress></Affiliation><Affiliation ID="Aff5"><OrgDivision>Department of Languages and Sciences of the Computation E.T.S. de Ingeniería Informática</OrgDivision><OrgName>University of Málaga</OrgName><OrgAddress><Street>Campus de Teatinos</Street><Postcode>29071</Postcode><City>Málaga</City><Country>Spain</Country></OrgAddress></Affiliation><Affiliation ID="Aff6"><OrgDivision>School of Cognitive and Computing Sciences</OrgDivision><OrgName>University of Sussex</OrgName><OrgAddress><City>Falmer</City><State>Brighton</State><Postcode>BN1 9QN</Postcode><Country>UK</Country></OrgAddress></Affiliation></EditorGroup></BookHeader><Part ID="Part3"><PartInfo TocLevels="0"><PartID>3</PartID><PartSequenceNumber>3</PartSequenceNumber><PartTitle>Contributions</PartTitle><PartChapterCount>80</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookID>3-540-45465-9</BookID><BookTitle>Automata, Languages and Programming</BookTitle></PartContext></PartInfo><Chapter ID="Chap56" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" Language="En" NumberingStyle="Unnumbered" TocLevels="0"><ChapterID>56</ChapterID><ChapterDOI>10.1007/3-540-45465-9_56</ChapterDOI><ChapterSequenceNumber>56</ChapterSequenceNumber><ChapterTitle Language="En">Infinite-State High-Level MSCs: Model-Checking and Realizability</ChapterTitle><ChapterSubTitle Language="En">Extended Abstract</ChapterSubTitle><ChapterFirstPage>657</ChapterFirstPage><ChapterLastPage>668</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2002</CopyrightYear></ChapterCopyright><ChapterHistory><RegistrationDate><Year>2002</Year><Month>6</Month><Day>24</Day></RegistrationDate><OnlineDate><Year>2002</Year><Month>6</Month><Day>25</Day></OnlineDate></ChapterHistory><ChapterGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant><AbstractGrant Grant="OpenAccess"></AbstractGrant><BodyPDFGrant Grant="Restricted"></BodyPDFGrant><BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant><BibliographyGrant Grant="Restricted"></BibliographyGrant><ESMGrant Grant="Restricted"></ESMGrant></ChapterGrants><ChapterContext><SeriesID>558</SeriesID><PartID>3</PartID><BookID>3-540-45465-9</BookID><BookTitle>Automata, Languages and Programming</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff7"><AuthorName DisplayOrder="Western"><GivenName>Blaise</GivenName><FamilyName>Genest</FamilyName></AuthorName></Author><Author AffiliationIDS="Aff7"><AuthorName DisplayOrder="Western"><GivenName>Anca</GivenName><FamilyName>Muscholl</FamilyName></AuthorName></Author><Author AffiliationIDS="Aff8"><AuthorName DisplayOrder="Western"><GivenName>Helmut</GivenName><FamilyName>Seidl</FamilyName></AuthorName></Author><Author AffiliationIDS="Aff7"><AuthorName DisplayOrder="Western"><GivenName>Marc</GivenName><FamilyName>Zeitoun</FamilyName></AuthorName></Author><Affiliation ID="Aff7"><OrgDivision>LIAFA</OrgDivision><OrgName>Université Paris VII</OrgName><OrgAddress><Street>2, pl. Jussieu, case 7014</Street><Postcode>75251</Postcode><City>Paris cedex 05</City><Country>France</Country></OrgAddress></Affiliation><Affiliation ID="Aff8"><OrgDivision>FB IV</OrgDivision><OrgName>Universität Trier</OrgName><OrgAddress><Postcode>54286</Postcode><City>Trier</City><Country>Germany</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>We consider three natural classes of infinite-state HMSCs: globally-cooperative, locally-cooperative and local-choice HMSCs. We show first that model-checking for globally-cooperative and locally-cooperative HMSCs has the same complexity as for the class of finite-state (bounded) HMSCs. Surprisingly, model-checking local-choice HMSCs turns out to be exponentially more efficient in space than for locally-cooperative HMSCs. We also show that locally-cooperative and local-choice HMSCs can be always implemented by communicating finite states machines, provided we allow some additional (bounded) message data. Moreover, the implementation of local-choice HMSCs is deadlock-free and of linear-size.</Para></Abstract><ArticleNote Type="Misc"><SimplePara>Work partly supported by the European research project IST-1999-29082 ADVANCE and by the INRIA/IRISA ARC project FISC.</SimplePara></ArticleNote></ChapterHeader><NoBody></NoBody></Chapter></Part></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Infinite-State High-Level MSCs: Model-Checking and Realizability</title><subTitle>Extended Abstract</subTitle></titleInfo><titleInfo type="alternative" contentType="CDATA" lang="en"><title>Infinite-State High-Level MSCs: Model-Checking and Realizability</title><subTitle>Extended Abstract</subTitle></titleInfo><name type="personal"><namePart type="given">Blaise</namePart><namePart type="family">Genest</namePart><affiliation>LIAFA, Université Paris VII, 2, pl. Jussieu, case 7014, 75251, Paris cedex 05, France</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Anca</namePart><namePart type="family">Muscholl</namePart><affiliation>LIAFA, Université Paris VII, 2, pl. Jussieu, case 7014, 75251, Paris cedex 05, France</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Helmut</namePart><namePart type="family">Seidl</namePart><affiliation>FB IV, Universität Trier, 54286, Trier, Germany</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Marc</namePart><namePart type="family">Zeitoun</namePart><affiliation>LIAFA, Université Paris VII, 2, pl. Jussieu, case 7014, 75251, Paris cedex 05, France</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre type="conference" displayLabel="OriginalPaper"></genre><originInfo><publisher>Springer Berlin Heidelberg</publisher><place><placeTerm type="text">Berlin, Heidelberg</placeTerm></place><dateIssued encoding="w3cdtf">2002-06-25</dateIssued><copyrightDate encoding="w3cdtf">2002</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><physicalDescription><internetMediaType>text/html</internetMediaType></physicalDescription><abstract lang="en">Abstract: We consider three natural classes of infinite-state HMSCs: globally-cooperative, locally-cooperative and local-choice HMSCs. We show first that model-checking for globally-cooperative and locally-cooperative HMSCs has the same complexity as for the class of finite-state (bounded) HMSCs. Surprisingly, model-checking local-choice HMSCs turns out to be exponentially more efficient in space than for locally-cooperative HMSCs. We also show that locally-cooperative and local-choice HMSCs can be always implemented by communicating finite states machines, provided we allow some additional (bounded) message data. Moreover, the implementation of local-choice HMSCs is deadlock-free and of linear-size.</abstract><relatedItem type="host"><titleInfo><title>Automata, Languages and Programming</title><subTitle>29th International Colloquium, ICALP 2002 Málaga, Spain, July 8–13, 2002 Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Peter</namePart><namePart type="family">Widmayer</namePart><affiliation>Institute of Theoretical Computer Science, ETH Zentrum, ETH Zürich, 8092, Zürich, Switzerland</affiliation><affiliation>E-mail: widmayer@inf.ethz.ch</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Stephan</namePart><namePart type="family">Eidenbenz</namePart><affiliation>Institute of Theoretical Computer Science, ETH Zentrum, ETH Zürich, 8092, Zürich, Switzerland</affiliation><affiliation>E-mail: eidenben@inf.ethz.ch</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Francisco</namePart><namePart type="family">Triguero</namePart><affiliation>Department of Languages and Sciences of the Computation E.T.S. de Ingeniería Informática, University of Málaga, Campus de Teatinos, 29071, Málaga, Spain</affiliation><affiliation>E-mail: triguero@lcc.uma.es</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Rafael</namePart><namePart type="family">Morales</namePart><affiliation>Department of Languages and Sciences of the Computation E.T.S. de Ingeniería Informática, University of Málaga, Campus de Teatinos, 29071, Málaga, Spain</affiliation><affiliation>E-mail: morales@lcc.uma.es</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Ricardo</namePart><namePart type="family">Conejo</namePart><affiliation>Department of Languages and Sciences of the Computation E.T.S. de Ingeniería Informática, University of Málaga, Campus de Teatinos, 29071, Málaga, Spain</affiliation><affiliation>E-mail: conejo@lcc.uma.es</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Matthew</namePart><namePart type="family">Hennessy</namePart><affiliation>School of Cognitive and Computing Sciences, University of Sussex, BN1 9QN, Falmer, Brighton, UK</affiliation><affiliation>E-mail: matthewh@cogs.susx.ac.uk</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="book-series" displayLabel="Proceedings"></genre><originInfo><copyrightDate encoding="w3cdtf">2002</copyrightDate><issuance>monographic</issuance></originInfo><subject><genre>Book-Subject-Collection</genre><topic authority="SpringerSubjectCodes" authorityURI="SUCO11645">Computer Science</topic></subject><subject><genre>Book-Subject-Group</genre><topic authority="SpringerSubjectCodes" authorityURI="I">Computer Science</topic><topic authority="SpringerSubjectCodes" authorityURI="I16005">Theory of Computation</topic><topic authority="SpringerSubjectCodes" authorityURI="I14002">Software Engineering/Programming and Operating Systems</topic><topic authority="SpringerSubjectCodes" authorityURI="I17001">Mathematics of Computing</topic><topic authority="SpringerSubjectCodes" authorityURI="I22013">Computer Graphics</topic><topic authority="SpringerSubjectCodes" authorityURI="I15009">Data Structures, Cryptology and Information Theory</topic></subject><identifier type="DOI">10.1007/3-540-45465-9</identifier><identifier type="ISBN">978-3-540-43864-9</identifier><identifier type="eISBN">978-3-540-45465-6</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="BookTitleID">72412</identifier><identifier type="BookID">3-540-45465-9</identifier><identifier type="BookChapterCount">90</identifier><identifier type="BookVolumeNumber">2380</identifier><identifier type="BookSequenceNumber">2380</identifier><identifier type="PartChapterCount">80</identifier><part><date>2002</date><detail type="part"><title>Contributions</title></detail><detail type="volume"><number>2380</number><caption>vol.</caption></detail><extent unit="pages"><start>657</start><end>668</end></extent></part><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2002</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Goos</namePart><affiliation>Karlsruhe University, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Juris</namePart><namePart type="family">Hartmanis</namePart><affiliation>Cornell University, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jan</namePart><namePart type="family">van Leeuwen</namePart><affiliation>Utrecht University, The Netherlands</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><copyrightDate encoding="w3cdtf">2002</copyrightDate><issuance>serial</issuance></originInfo><identifier type="ISSN">0302-9743</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2002</recordOrigin></recordInfo></relatedItem><identifier type="istex">B7048A9F0BD4AFA566C335DBAD928A1B93EEB33D</identifier><identifier type="DOI">10.1007/3-540-45465-9_56</identifier><identifier type="ChapterID">56</identifier><identifier type="ChapterID">Chap56</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 2002</accessCondition><recordInfo><recordContentSource>SPRINGER</recordContentSource><recordOrigin>Springer-Verlag Berlin Heidelberg, 2002</recordOrigin></recordInfo></mods></metadata></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Rhénanie/explor/UnivTrevesV1/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001148 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 001148 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Rhénanie
|area= UnivTrevesV1
|flux= Istex
|étape= Corpus
|type= RBID
|clé= ISTEX:B7048A9F0BD4AFA566C335DBAD928A1B93EEB33D
|texte= Infinite-State High-Level MSCs: Model-Checking and Realizability
}}
| This area was generated with Dilib version V0.6.31. |  |