LEADER 10807nam 22008055 450 001 996465762303316 005 20230329192159.0 010 $a3-319-72044-9 024 7 $a10.1007/978-3-319-72044-9 035 $a(CKB)4100000001381779 035 $a(DE-He213)978-3-319-72044-9 035 $a(MiAaPQ)EBC6287585 035 $a(MiAaPQ)EBC5591333 035 $a(Au-PeEL)EBL5591333 035 $a(OCoLC)1015335773 035 $a(PPN)222227818 035 $a(EXLCZ)994100000001381779 100 $a20171207d2017 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aRecent Trends in Algebraic Development Techniques$b[electronic resource] $e23rd IFIP WG 1.3 International Workshop, WADT 2016, Gregynog, UK, September 21?24, 2016, Revised Selected Papers /$fedited by Phillip James, Markus Roggenbach 205 $a1st ed. 2017. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2017. 215 $a1 online resource (X, 223 p. 28 illus.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v10644 300 $aIncludes index. 311 $a3-319-72043-0 327 $aIntro -- 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. 327 $aReferences -- 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. 327 $a4 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. 327 $a7 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. 330 $aThis 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. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v10644 606 $aComputer science 606 $aMachine theory 606 $aSoftware engineering 606 $aCompilers (Computer programs) 606 $aComputer simulation 606 $aMathematical logic 606 $aComputer Science Logic and Foundations of Programming 606 $aFormal Languages and Automata Theory 606 $aSoftware Engineering 606 $aCompilers and Interpreters 606 $aComputer Modelling 606 $aMathematical Logic and Foundations 615 0$aComputer science. 615 0$aMachine theory. 615 0$aSoftware engineering. 615 0$aCompilers (Computer programs). 615 0$aComputer simulation. 615 0$aMathematical logic. 615 14$aComputer Science Logic and Foundations of Programming. 615 24$aFormal Languages and Automata Theory. 615 24$aSoftware Engineering. 615 24$aCompilers and Interpreters. 615 24$aComputer Modelling. 615 24$aMathematical Logic and Foundations. 676 $a004 702 $aJames$b Phillip$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aRoggenbach$b Markus$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996465762303316 996 $aRecent Trends in Algebraic Development Techniques$9771917 997 $aUNISA