Leveraging Applications of Formal Methods, Verification and Validation. Rigorous Engineering of Collective Adaptive Systems 12th International Symposium, ISoLA 2024, Proceedings, Part II

Preface
Organization
Contents – Part II
Rigorous Engineering of Collective Adaptive Systems Introduction to the 5th Track Edition
	1 Collective Adaptive Systems
	2 Track Contributions
		2.1 Large Ensembles and Collective Dynamics
		2.2 Knowledge, Consciousness and Emergence
		2.3 Automated Reasoning for Better Interaction
		2.4 Modelling and Engineering Collective Adaptive Systems
		2.5 Analysing Collective Adaptive Systems
		2.6 Final Remarks
	References
Optimality-Preserving Reduction of Chemical Reaction Networks
	1 Introduction
	2 Controlled CRNs
	3 Species Equivalence of Controlled CRNs
		3.1 Lumping of CCRNs
	4 Optimality-Preserving Lumping
		4.1 Proof of Theorem 3
	5 Evaluation
	6 Conclusion
	References
Exploring Consensus Robustness in Swarms with Disruptive Individuals
	1 Introduction
	2 Methods
		2.1 Modelling Decision Making with Cross-Inhibition
		2.2 Bounded Linear Time Logic (BLTL)
		2.3 Formally Analysing Consensus with BLTL
	3 Results
		3.1 Robustness of Group Consensus in Presence of Stubborn Individuals
		3.2 Robustness of Group Consensus in Presence of Contrarian Individuals
		3.3 Robustness of Group Consensus in Presence of Stubborn and Contrarian Individuals
		3.4 Expected Time to Reach and Hold Majority in Presence of Stubborn and Contrarian Individuals
		3.5 Robustness of Group Consensus in Larger Groups
	4 Discussion and Future Work
	References
Towards Real-Time Aggregate Computing
	1 Introduction
	2 Background and Related Work
		2.1 Engineering Concurrent Spatially-Distributed Systems
		2.2 Aggregate Computing
		2.3 eXchange Calculus
		2.4 Formal Properties of Algorithms
		2.5 Real-Time Guarantees
	3 Composition of Behaviour
		3.1 Space-Time Independent Functions
		3.2 Discrete Space-Time Functions
		3.3 Continuous Space-Time Functions
		3.4 Mixing Continuous with Discrete
	4 Composition of Real-Time Specifications
		4.1 Discrete Space-Time Functions
		4.2 Continuous Space-Time Functions
		4.3 Guarantees for AP Building Blocks
	5 Conclusion and Future Work
	References
Epistemic Ensembles in Semantic and Symbolic Environments
	1 Introduction
	2 Epistemic Ensembles
	3 Dynamic Epistemic Ensemble Logic
	4 Action Models for Agent Actions
	5 Epistemic Ensembles in a Semantic Environment
	6 Epistemic Ensembles in a Symbolic Environment
	7 Relating Ensembles in Semantic and Symbolic Environments
	8 Conclusions
	References
The Evolving Conscious Agent, I
	1 Introduction
	2 Mendelian Genetics
		2.1 Population
		2.2 Reproduction
		2.3 A Little Genetics
		2.4 Mendel
		2.5 Justification
	3 Mutations
		3.1 Species
		3.2 Extending Mendel
		3.3 Mendelian Mutation
		3.4 Extinction
	4 Evolution
		4.1 Awareness
		4.2 Consciousness
		4.3 MendelAC
		4.4 Consciousness Evolving, MendelCE
		4.5 Correctness
	5 Related Work and Conclusion
	References
Emergence in Multi-agent Systems: A Safety Perspective
	1 Introduction
	2 Preliminaries
	3 Emergence in Multi-agent Systems
	4 Implementation
	5 Evaluation
	6 Related Work
	7 Conclusion
	References
The EM-BDD Algorithm For Learning Hidden Markov Models
	1 Introduction
	2 Binary Decision Diagrams
	3 Hidden Markov Models
	4 The EM-BDD Algorithm
		4.1 Building a BDD for an HMM and an Observation Sequence
		4.2 EM Part of EM-BDD
		4.3 Complexity Analysis
	5 Comparative Analysis of the EM-BDD and BW Algorithms
		5.1 Experimental Setup
		5.2 Findings
	6 Related Work
	7 Conclusions
	A  Calculating Edge Probabilities for Encoded Variables in BDD Representation
	B  Additional Experimental Results
	References
Is Machine Learning Model Checking Privacy Preserving?
	1 Introduction
	2 Signal Temporal Logic
	3 Learning Model Checking
		3.1 A Kernel for Signal Temporal Logic
		3.2 Learning Model Checking with the STL Kernel
	4 On the Information Leakage of Learning Model Checking
	5 Experiments
		5.1 Experimental Results
	6 Related Work
	7 Conclusion
	References
Matching Expectations in Ensembles: Connecting Verifiable Credentials and the Semantic Web
	1 Introduction
	2 Running Example
	3 Our Model
		3.1 Basic Notation
		3.2 Description Logics
		3.3 Modeling Assumptions, Expressions and Claims
	4 The Expectation Matching Problem
	5 Implementation
		5.1 Modeling Claims and Assumptions as Ontologies
		5.2 Infering New Statements by Reasoning
		5.3 Computing Solutions Through Querying
	6 Related Work
	7 Limitations
	8 Conclusion
	References
Once and for All: How to Compose Modules – The Composition Calculus
	1 Introduction
		1.1 The Problem
		1.2 The Idea of the Composition Calculus
		1.3 This Contribution
	2 The Notion of Modules
		2.1 Motivation
		2.2 Interfaces and Matches
		2.3 Graphs with Interfaces
		2.4 Modules
		2.5 Composition of Modules
		2.6 Equivalence
		2.7 Perfect Matches
	3 Algebraic Properties of Module Composition
		3.1 Associativity
		3.2 Cancelativity
		3.3 Commutativity
		3.4 Equidivisibility
		3.5 Neutral Module
	4 Classes of Modules
		4.1 Finitely Generated Sets of Modules
		4.2 Atomic Modules
		4.3 Abstract Modules
		4.4 Word Modules
	5 Related Work
	6 Conclusion
	References
RailCabs and Birds in Julia
	1 Introduction
	2 Background
		2.1 The Background of the Case Scenarios
	3 Introducing the Context-Role Library Contexts.jl
		3.1 Modeling RailCab Convoys with Contexts, Mixins, and Roles
		3.2 Modeling Starling Swarms with Contexts and Roles
	4 Discussion of the Approach
	5 Conclusion
	References
How Well Do LLMs Understand DEECo Ensemble-Based Component Architectures
	1 Introduction
	2 DEECo and Associated DSLs
		2.1 JDEECo and EDL
		2.2 TCOOF-ADL
		2.3 ML-DEECo
	3 Applying LLMs in Ensemble-Based Architecture Design and Development
		3.1 Methodology
		3.2 Question Structure
	4 Results, Discussion, and Observations
		4.1 Results Related to [RQ1]RQ1
		4.2 Results Related to [RQ2]RQ2:
		4.3 Results Related to [RQ3]RQ3
		4.4 Summary Answering [RQ1]RQ1, [RQ2]RQ2, [RQ3]RQ3
		4.5 Limitations and Threats to Validity
	5 Related Work
	6 Conclusion
	References
Model-Driven Development of Multi-Robot Systems: From BPMN Models to X-Klaim Code
	1 Introduction
	2 Background Notions
		2.1 BPMN Collaboration Diagrams
		2.2 X-Klaim
	3 The Translation Process
	4 The Translation at Work on an E-Agriculture Case Study
	5 The B2XKlaim Tool
	6 Related Works
	7 Concluding Remarks
	References
Rigorous Model Engineering of Hierarchical Multirate CPSs in MR-HybridSynchAADL
	1 Introduction
	2 Preliminaries
	3 The MR-HybridSynchAADL Language and Tool
	4 Formal Semantics of MR-HybridSynchAADL
		4.1 Representing MR-HybridSynchAADL Models
		4.2 Rewrite Rules
	5 Case Study: A Multirate Packet Delivery System
		5.1 System Description
		5.2 The MR-HybridSynchAADL Model
		5.3 Formal Analysis
	6 Related Work
	7 Concluding Remarks
	References
An Approach for Extended Swarm Formation Flight with Drones: PROTEASE2.0
	1 Introduction
	2 A Brief Description of Protease
	3 Related Work
	4 Approach
		4.1 Running Example: The Ring-of-Fliers
		4.2 Extension with Multiple Reference Points
		4.3 Extension with Hierarchies
	5 Proof of Concepts
		5.1 Evaluation Environment
		5.2 Experiments
		5.3 Multiple Reference Points: The Flower Pattern
		5.4 Multiple Reference Points: The Olympic Ring Pattern
		5.5 Hierarchies: Ring-of-Rings
		5.6 Discussion and Real-World Limitations
	6 Conclusion and Future Work
	References
Monitoring Local and Global Properties of Collective Adaptive Systems
	1 Introduction
	2 Flock Behaviour
	3 YODA: Yet anOther agent Description lAnguage
	4 Specifying Local and Global Properties in GLoTL
	5 Monitoring GLoTL formulas
	6 Related Work
	7 Conclusions
	References
Rigorous Analysis of Idealised Pathfinding Ants in Higher-Order Logic
	1 Introduction
	2 Basic Formalisations
		2.1 Environment
		2.2 Ants
	3 Specification
		3.1 System Description and Pheromone Release
		3.2 Behaviour of an Ant
		3.3 Compositional Dynamics
	4 Simulation
		4.1 Exploring the Behaviour of a Minimal Colony
	5 Logical Verification
		5.1 Minimal Invariant: Stigmergy Preservation
		5.2 Collective Convergence
	6 Conclusions and Related Work
	References
Statistical Model Checking of Cooperative Autonomous Driving Systems
	1 Introduction
	2 Related Work
	3 Background
		3.1 Statistical Model Checking
		3.2 The UPPAAL Model Checker For Timed Automata
		3.3 Cooperative Adaptive Cruise Control and Platooning
	4 Platoon Model In UPPAAL
		4.1 Leader Dynamic
		4.2 Platoon Commands
		4.3 Follower Dynamic
		4.4 Simulation Control
	5 Simulation and Probabilistic Verification
		5.1 Functional and Safety Properties
	6 Conclusion
	References
Attributed Point-to-Point Communication in R-CHECK
	1 Introduction
	2 Background Materials
		2.1 The ReCiPe Formalism
		2.2 The R-CHECK Language
	3 Extending ReCiPe & R-CHECK with Attributed Point-to-Point Communication
	4 Model Checking Point-to-Point LTOL Formulas
	5 The Superiority of Attributed Point-to-Point
	6 Concluding Remarks
	References
Local Reasoning and Attribute-Based Memory Updates for Enforcing Global Invariants in Collective Adaptive Systems
	1 Introduction
	2 Attribute-Based Memory Updates and CASs
		2.1 The AbU Calculus
		2.2 CAS Examples in AbU
	3 Distributed Verification of System-Level Invariants
		3.1 From Global to Local Invariants
		3.2 Aerial Drone Coalition
	4 Priority Scheduling and Correctness Guarantees
		4.1 A Scheduling Strategy for Priority Ordering
		4.2 Soundness of Local Invariants
	5 Conclusion
	References
Author Index