10807nam 22008055 450 99646576230331620230329192159.03-319-72044-910.1007/978-3-319-72044-9(CKB)4100000001381779(DE-He213)978-3-319-72044-9(MiAaPQ)EBC6287585(MiAaPQ)EBC5591333(Au-PeEL)EBL5591333(OCoLC)1015335773(PPN)222227818(EXLCZ)99410000000138177920171207d2017 u| 0engurnn|008mamaatxtrdacontentcrdamediacrrdacarrierRecent Trends in Algebraic Development Techniques[electronic resource] 23rd IFIP WG 1.3 International Workshop, WADT 2016, Gregynog, UK, September 21–24, 2016, Revised Selected Papers /edited by Phillip James, Markus Roggenbach1st ed. 2017.Cham :Springer International Publishing :Imprint: Springer,2017.1 online resource (X, 223 p. 28 illus.) Theoretical Computer Science and General Issues,2512-2029 ;10644Includes index.3-319-72043-0 Intro -- Preface -- Organization -- Contents -- Abstracts of Invited Talks -- Advances in Verification of Multi-agent Systems -- References -- The Distributed Ontology, Model and Specification Language - DOL -- References -- Full Papers of Invited Talks -- Theorising Monitoring: Algebraic Models of Web Monitoring in Organisations -- 1 Introduction -- 2 Concepts and Principles of Monitoring and Interventions -- 2.1 The Approach -- 2.2 Conceptual Framework for Monitoring -- 3 Monitoring Behaviour Modelled by Streams -- 3.1 Monitoring Streams -- 3.2 Storage -- 3.3 Interventions for Streams -- 4 Monitoring in Organisations -- 4.1 Why Employee Monitoring? -- 4.2 What Might Be Monitored and How? -- 4.3 Organisational Web Monitoring -- 5 Stream Model of Organisation Monitoring: Context -- 5.1 Organisation: Entities, Identity and Characteristics -- 5.2 Web Examples -- 5.3 Modelling Web Behaviour -- 6 Stream Model of Organisation Monitoring: Observation, Judgement, Monitoring -- 6.1 Web Content Observation -- 6.2 Data Usage Observation -- 6.3 Records -- 6.4 Monitoring -- 7 Stream Model of Organisation Monitoring: Storage -- 7.1 Histories, Thresholds and Queries -- 7.2 Data and Operations for Storage -- 8 Interventions -- 9 Concluding Remarks -- 9.1 The Monitoring Stack -- 9.2 Next Steps -- References -- Survey Papers -- Asymmetric Combination of Logics is Functorial: A Survey -- 1 Introduction -- 1.1 Motivation and Context -- 1.2 Contributions and Roadmap -- 2 Combination of Logics: A Brief Overview -- 3 Asymmetric Combination of Logics (Institutionally) -- 3.1 Institutions -- 3.2 An Institutional Rendering of Asymmetric Combinations of Logics -- 4 Asymmetric Combinations of Logics as Functors -- 4.1 Lifting Comorphisms -- 4.2 Property Preservation (Conservativity and Equivalence) -- 4.3 Natural Transformations -- 5 Conclusions and Future Work.References -- Algebraic Model Management: A Survey -- 1 Introduction -- 2 Model Management -- 2.1 Schema Mapping -- 2.2 Query Generation -- 2.3 Mapping Inversion -- 2.4 Mapping Composition -- 2.5 Schema Matching -- 2.6 Further References -- 3 Algebraic Model Management -- 3.1 Algebraic Databases -- 3.2 Schema Mapping -- 3.3 Query Generation -- 3.4 Mapping Composition -- 3.5 Mapping Inversion -- 3.6 Schema Matching -- 4 Conclusion -- References -- Regular Papers -- Probability Functions in the Context of Signed Involutive Meadows (Extended Abstract) -- 1 Introduction -- 1.1 A Survey of Design Options for the Inverse of 0 -- 1.2 Working with Involutive Ring Based Meadows -- 2 Boolean Algebras and Meadows -- 2.1 Boolean Algebras -- 2.2 Valuated Boolean Algebras and Some Naming Conventions -- 2.3 Events and Signed Meadows -- 3 Signed Meadow Based Probability Calculus -- 3.1 Equational Axioms for a Probability Function -- 3.2 Conditional Probability as a Total Operator: Four Options -- 3.3 Independence of Events -- 4 Logical Aspects of Equations for Probability Functions -- 4.1 Completeness of BA+Md+Sign+PFP -- 4.2 Using Free Boolean Algebras as Event Spaces -- 5 Multi-dimensional Probability Functions -- 5.1 Equational Axioms for a Probability Function Family -- 5.2 Existence of a Universal Probability Function -- 6 Concluding Remarks -- References -- A Calculus of Virtually Timed Ambients -- 1 Introduction -- 2 Virtually Timed Ambients -- 3 Comparing Virtually Timed Ambients -- 4 Related Work -- 5 Concluding Remarks -- References -- An Institution for Event-B -- 1 Introduction and Motivation -- 1.1 Formal Specification of a Traffic-Lights System in Event-B -- 1.2 Related Work: Institutions and Modularisation -- 2 An Institution for Event-B -- 2.1 Defining EVT -- 3 Relating FOPEQ and EVT -- 3.1 Pushouts and Amalgamation.4 Modularising Event-B Specifications -- 4.1 Refinement in the EVT Institution -- 4.2 A Modular, Refined Specification -- 5 Conclusion and Future Work -- References -- On the Most Suitable Axiomatization of Signed Integers -- 1 Introduction -- 2 Definitions of N -- 3 Approach 1: Definition of Z Using Set Theory -- 4 Formal Definitions -- 4.1 Syntactic Notations -- 4.2 Semantic Denotations -- 5 Definitions of Z Using Non-free Constructors -- 5.1 Approach 2: NF21 - Two Sorts and One Non-free Constructor -- 5.2 Approach 3: NF13 - One Sort and Three Non-free Constructors -- 5.3 Approach 4: NF31 - Three Sorts and One Non-free Constructor -- 5.4 Approach 5: NF22 - Two Sorts and Two Non-free Constructors -- 6 Definitions of Z Using Free Constructors -- 6.1 Approach 6: F32 - Three Sorts and Two Free Constructors -- 6.2 Approach 7: F23 - Two Sorts and Three Free Constructors -- 6.3 Approach 8: F22 - Two Sorts and Two Free Constructors -- 6.4 Approach 9: F21 - Two Sorts and One Constructor -- 6.5 Approach 10: F13 - One Sort and Three Free Constructors -- 7 Conclusion -- References -- Observational Semantics for Dynamic Logic with Binders -- 1 Introduction -- 2 D"3223379 -Logic: Background and Motivations -- 2.1 Overview on D"3223379 -- 2.2 Motivations -- 3 D"3223379 -Logic -- 3.1 Observational Models Category -- 3.2 Observational Satisfaction -- 4 Recovering Modal Invariance for Bisimulation -- 5 Relating Abstractor and Observational Semantics -- 6 Conclusion -- References -- Towards Critical Pair Analysis for the Graph Programming Language GP 2 -- 1 Introduction -- 2 Graphs and Graph Programs -- 2.1 Background -- 2.2 Example: Recognition of Series-Parallel Graphs -- 3 Unification of GP 2 List Expressions -- 4 Symbolic Critical Pairs -- 5 Construction and Finiteness of Symbolic Critical Pairs -- 6 Completeness of Symbolic Critical Pairs.7 Conclusion and Future Work -- References -- Canonical Selection of Colimits -- 1 Introduction -- 2 Preliminaries -- 2.1 Categories with Symbols -- 2.2 Specification Operators with Colimit Semantics -- 3 Desirable Properties of Colimit Selections -- 3.1 Symbols of a Diagram -- 3.2 Properties of Colimit Selections -- 4 Colimit Selections for Typical Signature Categories -- 4.1 Sets -- 4.2 Product Categories -- 4.3 Split Fibrations -- 5 Categories for Improved Colimit Selection -- 5.1 Named Specifications -- 5.2 Structured Symbol Names -- 6 Conclusion -- References -- Formalizing and Validating the P-Store Replicated Data Store in Maude* -- 1 Introduction -- 2 Preliminaries: Maude -- 3 Atomic Multicast in Maude -- 3.1 Atomic Multicast in Maude: ``User Interface'' -- 3.2 Maude Specification of Atomic Multicast -- 4 P-Store -- 4.1 P-Store in Detail -- 5 Formalizing P-Store in Maude -- 5.1 Class Declarations -- 5.2 Local Execution of a Transaction -- 5.3 Certification Phase -- 6 Formal Analysis of P-Store -- 7 Fixing P-Store -- 8 Related Work -- 9 Concluding Remarks -- References -- Generic Hoare Logic for Order-Enriched Effects with Exceptions -- 1 Introduction -- 2 Preliminaries: Monads and Exceptions -- 3 Order-Enrichment and Innocence -- 4 A Computational Metalanguage -- 5 Semantics -- 6 Hoare Calculus -- 7 Conclusion and Further Work -- References -- Author Index.This book constitutes the thoroughly refereed post-conference proceedings of the 23rd IFIP WG 1.3 International Workshop on Algebraic Development Techniques, WADT 2016, held in September 2016 in Gregynog, UK. The 9 revised papers presented together with two invited talks, one invited paper and two survey  papers were carefully reviewed and selected from numerous submissions and focus on foundations of algebraic specification; other approaches to formal specification, including process calculi and models of concurrent, distributed and mobile computing; specification languages, methods, and environments; semantics of conceptual modeling methods and techniques; model-driven development; graph transformations, term rewriting and proof systems; integration of formal specification techniques; formal testing and quality assurance, validation, and verification areas, broadly falling into three categories: multimedia content analysis; multimedia signal processing and communications; and multimedia applications and services.Theoretical Computer Science and General Issues,2512-2029 ;10644Computer scienceMachine theorySoftware engineeringCompilers (Computer programs)Computer simulationMathematical logicComputer Science Logic and Foundations of ProgrammingFormal Languages and Automata TheorySoftware EngineeringCompilers and InterpretersComputer ModellingMathematical Logic and FoundationsComputer science.Machine theory.Software engineering.Compilers (Computer programs).Computer simulation.Mathematical logic.Computer Science Logic and Foundations of Programming.Formal Languages and Automata Theory.Software Engineering.Compilers and Interpreters.Computer Modelling.Mathematical Logic and Foundations.004James Phillipedthttp://id.loc.gov/vocabulary/relators/edtRoggenbach Markusedthttp://id.loc.gov/vocabulary/relators/edtMiAaPQMiAaPQMiAaPQBOOK996465762303316Recent Trends in Algebraic Development Techniques771917UNISA