Foundations of Software Science and Computational Structures : 12th International Conference, FOSSACS 2009, Held As Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009, Proceedings

Annotation This book constitutes the refereed proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2009, held in York, UK, in March 2009, as part of ETAPS 2009, the European Joint Conferences on Theory and Practice of Software. The 30 revised full papers presented together with two invited talks were carefully reviewed and selected from 102 full paper submissions. The topics addressed are semantics, logics and automata, algebras, automata theory, processes and models, security, probabilistic and quantitative models, synthesis, and program analysis and semantics Front Matter....Pages - Facets of Synthesis: Revisiting Church’s Problem....Pages 1-14 Temporal Reasoning about Program Executions....Pages 15-15 Least and Greatest Fixpoints in Game Semantics....Pages 16-31 Full Abstraction for Reduced ML....Pages 32-47 Logics and Bisimulation Games for Concurrency, Causality and Conflict....Pages 48-62 Separating Graph Logic from MSO....Pages 63-77 On the Completeness of Dynamic Logic....Pages 78-91 Dependency Tree Automata....Pages 92-106 On Global Model Checking Trees Generated by Higher-Order Recursion Schemes....Pages 107-121 A Kleene Theorem for Polynomial Coalgebras....Pages 122-136 Coalgebraic Hybrid Logic....Pages 137-151 A Description of Iterative Reflections of Monads (Extended Abstract)....Pages 152-166 Tighter Bounds for the Determinisation of Büchi Automata....Pages 167-181 Lower Bounds on Witnesses for Nonemptiness of Universal Co-Büchi Automata....Pages 182-196 Interrupt Timed Automata....Pages 197-211 Parameter Reduction in Grammar-Compressed Trees....Pages 212-226 The Calculus of Handshake Configurations....Pages 227-241 On the Expressive Power of Restriction and Priorities in CCS with Replication....Pages 242-256 Normal Bisimulations in Calculi with Passivation....Pages 257-271 Reactive Systems, Barbed Semantics, and the Mobile Ambients....Pages 272-287 On the Foundations of Quantitative Information Flow....Pages 288-302 Cryptographic Protocol Composition via the Authentication Tests....Pages 303-317 Bisimulation for Demonic Schedulers....Pages 318-332 On Omega-Languages Defined by Mean-Payoff Conditions....Pages 333-347 Minimal Cost Reachability/Coverability in Priced Timed Petri Nets....Pages 348-363 Delayed Nondeterminism in Continuous-Time Markov Decision Processes....Pages 364-379 Concurrency, σ -Algebras, and Probabilistic Fairness....Pages 380-394 Synthesis from Component Libraries....Pages 395-409 Realizability of Concurrent Recursive Programs....Pages 410-424 Beyond Shapes: Lists with Ordered Data....Pages 425-439 Interprocedural Dataflow Analysis over Weight Domains with Infinite Descending Chains....Pages 440-455 Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types....Pages 456-470 Back Matter....Pages -