Recent Trends in Algebraic Development Techniques

Name: Recent Trends in Algebraic Development Techniques | 23rd IFIP WG 1.3 International Workshop, WADT 2016, Gregynog, UK, September 21-24, 2016, Revised Selected Papers
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

23rd IFIP WG 1.3 International Workshop, WADT 2016, Gregynog, UK, September 21-24, 2016, Revised Selected Papers

Phillip James Markus Roggenbach(Herausgeber*in)

Springer (Verlag)

Erschienen am 7. Dezember 2017

X, 223 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-72044-9 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

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

Systemvoraussetzungen

Als PDF speichern Als Link merken