Lecture Notes in Computer Science 7604 CommencedPublicationin1973 FoundingandFormerSeriesEditors: GerhardGoos,JurisHartmanis,andJanvanLeeuwen EditorialBoard DavidHutchison LancasterUniversity,UK TakeoKanade CarnegieMellonUniversity,Pittsburgh,PA,USA JosefKittler UniversityofSurrey,Guildford,UK JonM.Kleinberg CornellUniversity,Ithaca,NY,USA AlfredKobsa UniversityofCalifornia,Irvine,CA,USA FriedemannMattern ETHZurich,Switzerland JohnC.Mitchell StanfordUniversity,CA,USA MoniNaor WeizmannInstituteofScience,Rehovot,Israel OscarNierstrasz UniversityofBern,Switzerland C.PanduRangan IndianInstituteofTechnology,Madras,India BernhardSteffen TUDortmundUniversity,Germany MadhuSudan MicrosoftResearch,Cambridge,MA,USA DemetriTerzopoulos UniversityofCalifornia,LosAngeles,CA,USA DougTygar UniversityofCalifornia,Berkeley,CA,USA GerhardWeikum MaxPlanckInstituteforInformatics,Saarbruecken,Germany Jos C. M. Baeten Tom Ball Frank S. de Boer (Eds.) Theoretical Computer Science 7th IFIPTC 1/WG 2.2 International Conference,TCS 2012 Amsterdam, The Netherlands, September 26-28, 2012 Proceedings 1 3 VolumeEditors JosC.M.Baeten CentrumWiskunde&Informatica(CWI) SciencePark123,1098XGAmsterdam,TheNetherlands E-mail:[email protected] TomBall MicrosoftResearch OneMicrosoftWay,Redmond,WA98052,USA E-mail:[email protected] FrankS.deBoer CentrumWiskunde&Informatica(CWI) SciencePark123,1098XGAmsterdam,TheNetherlands E-mail:[email protected] ISSN0302-9743 e-ISSN1611-3349 ISBN978-3-642-33474-0 e-ISBN978-3-642-33475-7 DOI10.1007/978-3-642-33475-7 SpringerHeidelbergDordrechtLondonNewYork LibraryofCongressControlNumber:2012946731 CRSubjectClassification(1998):F.1.1-2,F.4.3,F.2.2,F.4.1,G.2.2 LNCSSublibrary:SL1–TheoreticalComputerScienceandGeneralIssues ©IFIPInternationalFederationforInformationProcessing2012 Thisworkissubjecttocopyright.Allrightsarereserved,whetherthewholeorpartofthematerialis concerned,specificallytherightsoftranslation,reprinting,re-useofillustrations,recitation,broadcasting, reproductiononmicrofilmsorinanyotherway,andstorageindatabanks.Duplicationofthispublication orpartsthereofispermittedonlyundertheprovisionsoftheGermanCopyrightLawofSeptember9,1965, initscurrentversion,andpermissionforusemustalwaysbeobtainedfromSpringer.Violationsareliable toprosecutionundertheGermanCopyrightLaw. Theuseofgeneraldescriptivenames,registerednames,trademarks,etc.inthispublicationdoesnotimply, evenintheabsenceofaspecificstatement,thatsuchnamesareexemptfromtherelevantprotectivelaws andregulationsandthereforefreeforgeneraluse. Typesetting:Camera-readybyauthor,dataconversionbyScientificPublishingServices,Chennai,India Printedonacid-freepaper SpringerispartofSpringerScience+BusinessMedia(www.springer.com) Preface TheconferenceTCS2012,the7thIFIPInternationalConferenceonTheoretical Computer Science, was organisedby IFIP TechnicalCommittee 1 (Foundations of Computer Science) and its 9 working groups, and IFIP Working Group 2.2 (FormalDescriptionsofProgrammingConcepts),andwasassociatedtotheIFIP World Computing Congress, also held in Amsterdam in the same week. The TCS conference provides a meeting place for the theoretical computer science communitywherethelatestresultsincomputationtheorycanbepresentedand more broadly experts in theoretical computer science can get together to share insightsandaskquestionsaboutthefuturedirectionsofthefield.TCS2012was associated with The Alan Turing Year 2012. Previous conferences of this series were held in Sendai (2000), Montreal (2002), Toulouse (2004), Santiago (2006), Milan (2008), and Brisbane (2010). This volume contains the papers presented at the TCS conference held on September 26–28, 2012, hosted by the Centrum Wiskunde & Informatica in Amsterdam. There were 48 submissions. Each submission was reviewed by 3 programcommittee members (exceptionally,by 4 or 2). The committee decided to accept 25 papers. The conference program also included 3 invited talks by Rajeev Alur, Yuri Gurevich, and Jiri Wiedermann. TCS 2012 was sponsored by the International Federation for Information Processing(IFIP),theNetherlandsOrganisationforScientificResearch(NWO), Microsoft Research, the Institute for Programming research and Algorithmics (IPA), and Centrum Wiskunde & Informatica (CWI). Wethankthemembersoftheprogramcommitteeandtheadditionalreview- ers for their work, the invited speakers for their contributions, and all authors who submitted their work to TCS 2012. July 2012 Jos C.M. Baeten Tom Ball Frank S. de Boer Organization Program Committee Jos C.M. Baeten Centrum Wiskunde & Informatica Tom Ball Microsoft Research Ahmed Bouajjani LIAFA, University of Paris 7 (Paris Diderot) Ana Cavalcanti University of York Frank S. De Boer Centrum Wiskunde & Informatica Susanne Graf Universit´e Joseph Fourier / CNRS / VERIMAG Peter Gruenwald Centrum Wiskunde & Informatica Juraj Hromkovic ETH Zurich Jan Ju¨rjens TU Dortmund and Fraunhofer ISST Joseph Kiniry IT University of Copenhagen Martin Kutrib Universita¨t Giessen Aart Middeldorp University of Innsbruck Ugo Montanari Universita` di Pisa Peter Mu¨ller ETH Zu¨rich David Naumann Stevens Institute of Technology Catuscia Palamidessi INRIA and LIX, Ecole Polytechnique Jan Rutten Centrum Wiskunde & Informatica Davide Sangiorgi University of Bologna Jeffrey Shallit University of Waterloo Leen Torenvliet University of Amsterdam Igor Walukiewicz CNRS, LaBRI Jim Woodcock University of York Additional Reviewers Andova, Suzana Cairns, Paul Atig, Mohamed Faouzi Cimini, Matteo Bergfeld, Jort Courcelle, Bruno Bodlaender, Hans Dal Lago, Ugo Boeckenhauer,Hans-Joachim De Liguoro, Ugo Bonchi, Filippo de Wolf, Ronald Bonsangue, Marcello Enea, Constantin Bors, Adrian Fantechi, Alessandro Brengos, Tomasz Felgenhauer, Bertram Bruni, Roberto Fenner, Stephen Butterfield, Andrew Fijalkow, Nathana¨el Caires, Luis Fiore, Marcelo VIII Organization Fokkink, Wan Martin, Barnaby Foniok, Jan Meckel, Katja Foster, Simon Miller, Dale Freitas, Leo Montanaro, Ashley Gebauer, Heidi Mytkowicz, Todd Geuvers, Herman Neurauter, Friedrich Gouw, Stijn Pirandola, Stefano Hansen, Helle Rispal, Chlo´e Herbreteau, Fr´ed´eric Rossmanith, Peter Hirschkoff, Daniel Rot, Jurriaan Holzer, Markus Rutten, Jan Horbach, Matthias Salvati, Sylvain Jaghoori,Mohammad Mahdi Sammartino, Matteo Jakobi, Sebastian Sangnier, Arnaud Jongmans, Sung-Shik T.Q. Scho¨pp, Ulrich Kameyama,Yukiyoshi Silva, Alexandra Keller, Lucia Smula, Jasmin Kishida, Kohei Sobocinski, Pawel Klin, Bartek Steffen, Bjo¨rn Komm, Dennis Sternagel, Christian Kosowski,Adrian Thiemann, Ren´e Kratsch, Dieter Truthe, Bianca Krug, Sacha Ummels, Michael Loreti, Michele van Leeuwen, Erik Jan Lozes, Etienne Van Raamsdonk, Femke Luettgen, Gerald Vicario, Enrico Mackie, Ian Winter, Joost Malcher, Andreas Zantema, Hans Markovski,Jasen Zhang, Lijun Table of Contents Computability and Non-computability Issues in Amorphous Computing...................................................... 1 Jiˇr´ı Wiedermann Static Single Information Form for Abstract Compilation ............. 10 Davide Ancona and Giovanni Lagorio Input-Driven Stack Automata ..................................... 28 Suna Bensch, Markus Holzer, Martin Kutrib, and Andreas Malcher Probabilistic Inference and Monadic Second Order Logic.............. 43 Marijke Hans L. Bodlaender Cinderella versus the Wicked Stepmother ........................... 57 Marijke Hans L. Bodlaender, Cor A.J. Hurkens, Vincent J.J. Kusters, Frank Staals, Gerhard J. Woeginger, and Hans Zantema Worst- and Average-Case Privacy Breaches in Randomization Mechanisms ..................................................... 72 Michele Boreale and Michela Paolini Weak Bisimulations for Coalgebras over Ordered Functors............. 87 Tomasz Brengos A Context-Free Linear Ordering with an Undecidable First-Order Theory............................................... 104 Arnaud Carayol and Zolta´n E´sik Open Bisimulation for Quantum Processes .......................... 119 Yuxin Deng and Yuan Feng A Modular LTS for Open Reactive Systems ......................... 134 Fabio Gadducci, Giacoma Valentina Monreale, and Ugo Montanari Unidirectional Channel Systems Can Be Tested...................... 149 Petr Janˇcar, Prateek Karandikar, and Philippe Schnoebelen On Properties and State Complexity of Deterministic State-Partition Automata....................................................... 164 Galina Jira´skova´ and Tom´aˇs Masopust On Union-Free and Deterministic Union-Free Languages .............. 179 Galina Jira´skova´ and Benedek Nagy X Table of Contents A Characterisation of Languages on Infinite Alphabets with Nominal Regular Expressions.............................................. 193 Alexander Kurz, Tomoyuki Suzuki, and Emilio Tuosto Formal Verification of Distributed Algorithms: From Pseudo Code to Checked Proofs .................................................. 209 Philipp Ku¨fner, Uwe Nestmann, and Christina Rickmann A Temporal Logic for Multi-threaded Programs...................... 225 Salvatore La Torre and Margherita Napoli The Algorithmic Complexity of k-Domatic Partition of Graphs ........ 240 Hongyu Liang Unique Parallel Decomposition in Branching and Weak Bisimulation Semantics....................................................... 250 Bas Luttik Modal Interface Automata ........................................ 265 Gerald Lu¨ttgen and Walter Vogler Proofs as Executions ............................................. 280 Emmanuel Beffara and Virgile Mogbil Efficient Algorithms for the max k-vertex cover Problem........... 295 Federico Della Croce and Vangelis Th. Paschos A Model Theoretic Proof of Completeness of an Axiomatization of Monadic Second-Order Logic on Infinite Words ...................... 310 Colin Riba Compositional Abstraction Techniques for Probabilistic Automata ..... 325 Falak Sher and Joost-Pieter Katoen BroadcastAbstraction in a Stochastic Calculus for Mobile Networks.... 342 Lei Song and Jens Chr. Godskesen An Intersection Type System for Deterministic Pushdown Automata ... 357 Takeshi Tsukada and Naoki Kobayashi An Output-Based Semantics of Λμ with Explicit Substitution in the π-Calculus: Extended Abstract .................................... 372 Steffen van Bakel and Maria Grazia Vigliotti Errata Probabilistic Inference and Monadic Second Order Logic.............. E1 Marijke Hans L. Bodlaender Cinderella versus the Wicked Stepmother ........................... E2 Marijke Hans L. Bodlaender, Cor A.J. Hurkens, Vincent J.J. Kusters, Frank Staals, Gerhard J. Woeginger, and Hans Zantema Author Index.................................................. 389 Computability and Non-computability Issues (cid:2) in Amorphous Computing Jiˇr´ıWiedermann InstituteofComputerScience,AcademyofSciencesoftheCzechRepublic, PodVoda´renskouveˇzˇ´ı2,18207Prague8,CzechRepublic [email protected] Abstract. Amorphous computing systems consist of a huge set of tinysimple stationaryor mobileprocessors whosecomputational, communication andsen- sory part is reduced to an absolute minimum. In an airborne medium the pro- cessorscommunicateviaashort-rangeradiowhileinawaterbornemediumvia molecular communication. Insomecasesthecomputational partoftheproces- sorscanbesimplifieddowntofinitestateautomataorevencombinatorialcircuits andthesystemasawholecanstillpossessuniversalcomputationalpowerwith ahighprobability.Wewillarguethattheamorphoussystemsbelongamongthe simplest(non-uniform)universalcomputationaldevices.Ontheotherhand,itis questionableastowhatextentthestandarduniversalmodelsofcomputationcan faithfullycapturethebehaviorofamorphouscomputingsystemswhosefunction- alityalsodependsonthenon-computational and/orunpredictableoperationsof certainpartsoftheentiresystem. 1 Introduction Thenotionofamorphouscomputingsystems,i.e.,ofcomputationalsystemslackingany concrete“architecture”,hasemergedbytheendofthe1990’s.Initially,thedevelopment ofsuchsystemsstartedasanengineeringenterprisemotivatedbytechnologicaladvance- ment in the field of micro-electro-mechanicalsystems, wireless communicationsand digitalelectronics(cf.[1],[2],[4],[5],[6],[7],[12],[13],[14]).Technologicalprogress enabledintegrationof sensing,data processingand wireless communicationcapabili- tiesintoasingleprocessor.Inthesesystemstheminiaturizationhasbeenpushedtoits limitsresulting,presumably,intoprocessorsofalmostmolecularsizewiththerespec- tivecommunicationandcomputingfacilitiesadequately(andthus,severely)restricted. These limitationsalone,and the factthat systemsconsisting of hugenumbersofpro- cessors are considered, have jointly called for the change of the basic computational andcommunicationparadigmsofdistributedcomputingsystems.Thesenewparadigms also seem to have a potential to challenge certain computability issues related to our understandingofcomputing. Nowadayswe see amorphouscomputingsystems in many forms(cf. [19]). Amor- phous computing systems typically consist of a huge set of tiny simple processors equipped with small memory, random number generator, simple wireless communi- cation means, sensors and an energysource. The processorsare randomlydistributed (cid:2)ThisworkwaspartiallysupportedbyRVO67985807andtheGACˇRgrantNo.P202/10/1333. J.C.M.Baeten,T.Ball,andF.S.deBoer(Eds.):TCS2012,LNCS7604,pp.1–9,2012. (cid:2)c IFIPInternationalFederationforInformationProcessing2012