Foundations of Software Science and Computation Structures: 16th International Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings

Title......Page 1
Foreword......Page 4
Preface......Page 10
Organization......Page 11
Ten Years of Amortized Resource Analysis......Page 15
 References......Page 16
Bisimulation......Page 18
  Introduction......Page 21
  Kappa and Implicit Deletion......Page 22
  Pattern Graphs......Page 25
  Kappa and -graphs......Page 27
   Encoding -graphs as Pattern Graphs......Page 29
  Coherence......Page 30
  Pushouts of -graphs......Page 34
  Conclusion......Page 35
  References......Page 36
  Introduction......Page 37
  Definitions and First Properties......Page 40
  Closure Properties, Emptiness and Universality......Page 44
  Weakening HRAs......Page 46
   Non-reset HRAs......Page 47
   Unary HRAs......Page 49
  Connections with Existing Formalisms......Page 50
  Further Directions and Acknowledgements......Page 51
  References......Page 52
  Introduction......Page 54
  Fatal Attractors......Page 56
  Partial Solvers......Page 58
   Partial Solver psolB......Page 59
   Partial Solver psolQ......Page 60
   Robustness of psolB......Page 63
   Experimental Setup......Page 64
   Experiments on Structured Games......Page 65
   Number of Detected Fatal Attractors......Page 67
  Conclusions......Page 68
  References......Page 69
  Introduction......Page 70
   Outline of the Paper......Page 71
   Applied -Calculus......Page 72
   Depth and Norm of Processes......Page 76
  Decomposition w.r.t. Strong Labeled Bisimilarity......Page 77
  Decomposition w.r.t. Weak Labeled Bisimilarity......Page 80
  Related Work......Page 82
  References......Page 83
  Introduction......Page 85
  Model......Page 88
   Multi-pushdown Systems......Page 90
   Bounded Context-Switching......Page 91
  Contextual Pushdown Counter Systems......Page 92
  Bounded Context-Switching Reachability......Page 95
  References......Page 99
  Introduction......Page 101
  Communicating Timed Processes......Page 104
  Decidability of Communicating Tick Automata......Page 105
  Decidability of Communicating Timed Automata......Page 111
  Conclusions and Future Work......Page 114
  References......Page 115
  Introduction......Page 117
  Value-Computation Bisimulation......Page 119
   Value-Computation Transition Systems......Page 120
   Congruence Format......Page 122
   MSOS Labels......Page 123
   MSOS Specifications......Page 124
   Bisimulation in MSOS......Page 127
   Congruence Format......Page 128
  Modular Bisimulations......Page 130
  Further Directions......Page 131
  References......Page 132
  Introduction......Page 133
  Graph Transformation with Borrowed Contexts......Page 134
  Attributed Graphs and Symbolic Graphs......Page 136
  Bisimilarity of Attributed Graphs and S-bisimilarity......Page 138
  An Inference System for Proving Bisimilarity......Page 139
  A Tableau Method for Checking Bisimilarity......Page 143
  Related Work and Conclusion......Page 146
  References......Page 148
  Introduction......Page 149
  Syntax and Behaviour for Stateful and Effectful Languages......Page 150
   Transition Systems for Stateful and Effectful Languages......Page 151
   Transition Systems, Categorically......Page 152
  Three Evaluation-in-Context Rule Formats......Page 154
   From EIC Specifications to Operational Models......Page 156
  Behavioural Equivalence in a Kleisli Category......Page 159
  Compositionality and Adequacy......Page 161
  Conclusion......Page 163
  References......Page 164
  Introduction......Page 165
  Preorders on Monads......Page 166
   The Category BRel of Binary Relations......Page 167
   Relational Liftings and Coalgebraic Simulations......Page 168
   Preorder -Lifting......Page 169
  Characterising Pre(T) as the Limit of a Large Chain......Page 171
    Computing CSPre(T,) with a Large Enough  for Preorder Axioms......Page 174
  Conclusion and Related Work......Page 178
  References......Page 179
Quantitative Models......Page 19
  Introduction......Page 181
  Probabilistic Concurrent Processes......Page 184
  Probabilistic Modal -Calculus (pL)......Page 185
  Proof System......Page 186
   Markov Proofs......Page 191
  Examples of Markov Proofs......Page 193
  Further Directions......Page 195
  References......Page 196
  Introduction......Page 197
  The Illative System......Page 198
   Representing Logic......Page 201
   Equality, Recursive Definitions and Extensionality......Page 202
   Induction and Natural Numbers......Page 203
  Conservativity and Consistency......Page 205
  Partiality and General Recursion......Page 208
   Relationship with Systems of Illative Combinatory Logic......Page 210
  Conclusion......Page 211
  References......Page 212
  Introduction......Page 213
  BAOs and Coalgebraic Logics......Page 214
  Presentations and Translations......Page 221
  The Translation Theorem......Page 222
  Sahlqvist Formulae for Coalgebraic Logics......Page 224
  Outlook......Page 227
  References......Page 228
  Introduction......Page 229
  Preliminaries......Page 230
  Nested Sequents for Intuitionistic Modal Logics......Page 232
  Soundness......Page 235
  Completeness......Page 239
  Cut Elimination......Page 240
  References......Page 243
  Introduction......Page 245
  Purity......Page 247
  The Total Case......Page 250
  The Partial Case......Page 253
   Domain of Strategy Trees......Page 254
   Representation Theorem......Page 255
  Generalizations......Page 256
  Applications......Page 257
  Conclusion......Page 258
  References......Page 259
  Introduction......Page 261
  Syntax of the Language......Page 263
  Game Model......Page 265
  Factorisation......Page 267
  Syntactic Transformation......Page 270
  When Integer References Suffice......Page 273
  When All References Are Dispensible......Page 275
  References......Page 276
  Introduction......Page 277
  The Language......Page 279
  Operational Semantics......Page 280
  Axiomatic Semantics......Page 285
  Soundness of the Axiomatic Semantics......Page 288
  Formalization in Coq......Page 290
  Conclusions and Further Research......Page 291
  References......Page 292
  Introduction......Page 293
  Post Embedding Problems......Page 295
   The Hardy Hierarchy......Page 297
   Encoding Hardy Configurations......Page 299
   Encoding Hardy Computations......Page 300
   Lower Bound......Page 302
   Upper Bound......Page 303
  Applications......Page 304
  Concluding Remarks......Page 306
  References......Page 307
  Introduction......Page 309
  Definitions......Page 311
   Problems of Interest......Page 312
  The BKW Algorithm......Page 313
   The Recursion Depth of BKW......Page 316
  The Definability Problem......Page 317
   Definability for REs and NFAs......Page 318
   Definability for RE(#)s......Page 321
   Definability for DFAs......Page 322
  References......Page 323
  Introduction......Page 325
   Informal Semantics......Page 327
   Semantics of Expressions, Configurations and Environments......Page 328
   Strong Normalization, Lock-Freedom and Confluence......Page 329
   Well-Typed Processes......Page 330
   Neutral, Max, and Positive Operators......Page 332
   Main Result......Page 333
   Process Runtime......Page 334
   Process Spawning......Page 335
   PSpace Abiding Evaluation Strategy......Page 336
  Completeness......Page 337
  Conclusion......Page 338
  References......Page 339
  Introduction......Page 341
  PURPLE and Extensions......Page 343
   Nondeterminism......Page 345
  Preliminaries......Page 347
  Main Result......Page 349
  Conclusion and Future Work......Page 354
  References......Page 355
  Introduction......Page 357
   Related Work......Page 359
  Syntax......Page 360
  Operational Semantics......Page 362
   Examples......Page 364
  Denotational Semantics......Page 365
   Logical Relations Characterisation......Page 368
   Subdomains......Page 369
   Function Definability......Page 370
  Conclusion......Page 371
  References......Page 372
  Introduction......Page 373
  Preliminaries......Page 375
  Quantile Queries......Page 376
  Evaluating Qualitative Queries......Page 378
   Existential Queries......Page 381
   Universal Queries......Page 384
   A Pseudo-polynomial Algorithm for Markov Chains......Page 386
  References......Page 387
  Introduction......Page 389
   Weighted Automata......Page 393
   Parameterized Weighted Containment......Page 394
   Geometry in IRk......Page 395
   The Two-Bound PWC Problem for Deterministic Automata......Page 397
   When B Is Not Given......Page 399
   The One-Bound PWC Problem for Deterministic Automata......Page 400
   The One-Bound PWC Problem for Nondeterministic Automata......Page 402
  References......Page 403
  Introduction......Page 405
  Preliminaries......Page 407
  Weighted Regular Expressions with Pebbles......Page 408
  Weighted Automata with Pebbles......Page 410
   Weighted First-Order Logic......Page 415
   Weighted Temporal Logics......Page 418
  Conclusion and Perspectives......Page 419
  References......Page 420
Categorical Models......Page 20
  Introduction......Page 421
   Signatures of Parameters......Page 424
   Parameterized Algebraic Theories......Page 425
   Presentation of Predicate Logic......Page 426
   Other Examples of Parameterized Algebraic Theories......Page 427
   Incompleteness of Set-Theoretic Models......Page 428
   Other Equational Approaches to Logic......Page 429
  Extending the Algebraic Theory to a Programming Language......Page 430
  Representation of Terms......Page 431
  Enriched Clones......Page 434
  References......Page 436
  Introduction......Page 438
  Event Structures and Stable Families......Page 439
  Process Operations......Page 441
  Pre-strategies......Page 442
   Concurrent Copy-cat......Page 443
   A New Characterization of Concurrent Strategies......Page 444
   The Scott Order in Games......Page 445
   Strategies in Games as Presheaves......Page 446
   Identity......Page 447
   Composition......Page 448
   Laxness......Page 449
  Games as Factorization Systems......Page 451
  References......Page 452
  Introduction......Page 454
  Nominal Sets......Page 456
  Separating Functions......Page 459
  Generalised Abstraction......Page 463
  When Do Separating Functions and Generalised Abstraction Coincide?......Page 464
  Applications and Further Work......Page 466
  References......Page 468
Author Index......Page 470