Saad Aldoihi
email: aldoihi@ensta.fr

Omar Hammami
email: hammami@ensta.fr

Effect of Invisible Exertions on Computed Tomography Radiologists in Saudi Hospitals

Keywords: invisible exertions, Evaluation of invisible exertion, CT scan invisible exertion, CT scan overload effects

Current radiology practices face extreme pressure on available resources with demands of multi-dimensional requirements. Technicians are at the center of a constant drive for optimal productivity and optimization with the minimal possible resources. This paper evaluates the invisible physical and mental exertions resulting from operating computed tomography (CT) scans by fifty-seven technicians surveyed following current radiology practices. Demographic characteristics were reviewed to evaluate differences across the study variables based on gender, level of education, years of experience, and working sector.

I. INTRODUCTION

The effects of physical and mental exertion on technicians working in radiology are overwhelming. Current radiology practice suffers from declining salaries, increasing workload, and workflow complexity [START_REF] Forman | Masters of radiology panel discussion: hyperefficient radiology-can we maintain the pace?[END_REF]. Although a radiology work environment is categorized as shift work, disturbances in daily sleeping cycles are associated with physiological and behavioral effects as well as a loss of the rhythm entrainment [START_REF] Berger | Impact of shift work on the health and safety of nurses and patients[END_REF]. Considerable fatigue and human error affect radiology practices with recent literature covering how diagnostic accuracy is compromised after long working hours [START_REF] Krupinski | Long radiology workdays reduce detection and accommodation accuracy[END_REF] [START_REF] Krupinski | Do long radiology workdays affect nodule detection in dynamic CT interpretation?[END_REF] [START_REF] Krupinski | The impact of fatigue on satisfaction of search in chest radiography[END_REF][3] [START_REF] Taylor-Phillips | Retrospective review of the drop in observer detection performance over time in lesion-enriched experimental studies[END_REF]. Under financial pressure, radiologists' practices are adopting a faster and more agile productivity style to accommodate larger workloads. Radiologists are now more likely to increase their interpretation error by 26.6% as opposed to 10% under average working speeds [START_REF] Sokolovskaya | The effect of faster reporting speed for imaging studies on the number of misses and interpretation errors: a pilot study[END_REF].

Radiology technicians today experience extreme pressure from many invisible exertion constraints, such as safety requirements, ethical practices, productivity and optimization requirements, system and technology requirements, and industry best practice adaptations. Regardless of the industry, most new requirements are driven by increasing safety [START_REF] Miller | Lessons from Another Industry: Aviation, Usability, and Medical Device Design[END_REF]. Technicians are expected to facilitate all requirements while retaining the integrity of daily tasks. CT scan working conditions are categorized into the following themes:

• Dim lighting • Small and confined control rooms • Safety standards and practices

• Facilitating Technology This study evaluates existing invisible physical and mental exertions experienced during CT scan operation and identifies demographic differences among the study participants, such as gender, age, years of experience, and working sector.

Furthermore, the study explores the type of invisible exertion as physical or mental. To the best of our knowledge, no previous research explored and evaluated these invisible exertion effects for CT technicians. As other researchers have not exploited the theme of this study, we expect this work can open a new arena of research for evaluating a variety of invisible exertions and their effects on working environments.

II. DESCRIPTION OF THE PROBLEM

The current state of hospitals demands a substantial amount of efficiency provided from a minimal amount of resources. So, radiologists today are working with multi-objective aims, such as safety and optimization of space and other resources, and exertions from various directions provide added pressure to radiologists. However, considerable pressure results from invisible sources. The working practice of CT scan radiologists demands proactivity and efficiency with daily operating routines that include helping bedridden patients move to the CT scan table, administrate the contrast media, and re-centering the position of the patient. Therefore, numerous such activities result as invisible exertions, which can be categorized as non-machine-related exertion. As hospital management teams strive to maximize productivity and optimize the intake of resources, identifying primary sources of invisible exertion is imperative to maximize productivity while minimizing human error.

In field observation, radiologists overcome invisible exertion through a variety of techniques and maneuvers. During a CT exam, extensive effort positioning the patient correctly on the CT table is required before the exam. Technicians are required to direct the patient to lay down on the CT table and ensure the patient is precisely centered. Often, after a technician has spent many hours of extensive operating exams, they may try to prevent invisible exertion by maneuvering the CT scanner instead of directly re-centering of each patient. So, without the need to configure a new exam for each patient, the technician modifies the previous exam for the new patient to avoid entering the exam room and re-centering the patient. Figure1 and Figure2 show this repeated series functionality. Figure 3 summarizes the various exertions required during a CT scan, and this study highlights the impact of these actions on the operating technicians.

III. METHODS

Eighteen hours of observational field visits were conducted at the Radiology Department in King Saud Medical City. This stage worked as a preliminary phase to collect and observe variables requirements.The purpose of the visits was to pinpoint the various sources of invisible physical and mental exertions. A questionnaire was also developed to measure invisible exertions in terms of the physical and mental aspects while operating a CT scanner.

Ethical approval was sought and approved by the Ministry of Health in Saudi Arabia after satisfying the legal requirements of the Ministry's Institutional Review Board. Also, ethical principles were maintained and preserved for confidentiality, anonymity, and the right to withdraw.

A. Participant

The study featured 57 radiology technologists who operate CT scans daily. The participants came from hospitals across all 13 regions. The genders comprised 50.9% male and 49.1% female with an age range from 20 to over 50 years. This range spread included 77.2% from 20 to 29 years, 15.8% from 30 to 39 years, 3.5% from 40 to 49 years old, and 3.5% over 50 years. Education comprises 3.5% as having earned a diploma, 86% with a bachelor's degree, and 10.5% with a master's degree. Years of experience consisted of 68.4% with 0 to 3 years, 8.8% with 4 to 7 years, 10.5% with 8 to 11 years, and 12.3% with more than 12 years. The working sectors included 87.7% in the public sector and 12.3% in the private sector.

B. Procedure

Following the initial on-site observations of CT operations, a survey consisting of two parts was developed to measure the invisible physical and mental exertions experienced while operating the CT scanner. The first part collected participant demographic characteristics, as reported in the previous section, and the second included participant responses for two invisible exertion measurements. A volunteer was recruited to visit the hospitals and offer a paper-based questionnaire. In addition, an electronic version of the questionnaire was developed and sent to the participants.

C. Measurement

The objective is to measure the physical and mental dimensions of invisible exertion. Table 1 describes these two dimensions each with three associated measurement attributes.

IV. RESULTS

A. Gender 1) Invisible Physcial Exertion: Male respondents (Mdn = 25.46) did not appear to differ from female (Mdn = 32.41) in the amount of transferring bedridden patients from a hospital bed onto a CT table (U = 307). However, males (Mdn = 24.84) did significantly differ from females (Mdn = 33.02) in preparing the examination room for the next patient (U = 289.5, z = -2.47, p= 0.013). Males (Mdn = 24.62) also significantly differed from females (Mdn = 33.22) in preparing and administering the contrast media for patients (U = 283.5, z = -2.35, p = 0.019). Figure 4 and 5 provide box plots for these differing variables. 2) Invisable Mental Exertion: A Mann Whitney test shows no difference between the males and females across all invisible mental variables.

B. Age

A Kruskal-Wallis test evaluated differences across the invisible physical and mental variables, and no significant differences were identified based on age groups

C. Level of Education

A Kruskal-Wallis test evaluated differences between three educational levels (diploma, bachelor's, and master's) regarding the participants helping transfer bedridden patients from a hospital bed onto the CT table. The test was significant H (2, N = 57) = 7.91, p =.01.

Follow-up tests were performed to examine pairwise differences among these education group to control for type I errors using the Bonferroni approach. The results of these tests indicate a significant difference between bachelor's and master's degrees as illustrated in Figure 6.

Additionally, the other invisible physical and mental variables do not appear to differ based on the level of education.

D. Years Of Expereince

A Kruskal-Wallis test was conducted to evaluate the difference between the groups with similar years of experience (0 to 3, 4 to 7, 8 to 11 years, and more than 12 years) on working in an understaffed environment. The test resulted in a significant H (3, N = 57) = 9.23, p = .02.

Follow-up tests were performed to examine the pairwise differences among these groups to control for type I errors across the tests using the Bonferroni approach. The results of these tests indicate significant differences between the 0 to 3 and 4 to 7 years groups and between the 0 to 3 years and more than 12 years groups as are illustrated in Figure 7.

Additional tests were conducted on the other invisible physical and mental variables with no differences identified. Additional tests were conducted on all invisible physical and mental variables and no differences were found.

E. Working Sector

The public sector technicians (Mdn = 31.15) appeared to differ from the private sector (Mdn = 13.64) in the response to the department needs more CT scan machines (U = 67.5, z = -2.7, p = .007) as is illustrated in Figure 8.

Additional tests were conducted on the other invisible physical and mental variables with no differences found. Additional tests were conducted on all invisible physical and mental variables and no differences were found.

V. CONCLUSION

Radiology practices are impacted by many challenges that eventually require more exertion on the operators. The current standards in practice are categorized to drive for more efficiency in terms of consuming resources as they try to maximize productivity and optimization. Many requirements have been added to the processes of radiology, such as safety and ethics, to compromise a minimum for industry best practice. These requirements now reflect on the working load of the technicians and add complexity to the overall process. This study identifies this additional exertion that affects the technician as is experienced through invisible exertion.

Fig. 1 :

 1 Fig. 1: Repeat Series

Fig. 4 :

 4 Fig. 4: Gender difference in preparing and administering the contrast media.

Fig. 5 :

 5 Fig. 5: Gender difference in preparing the exam room for the next patient.

Fig. 6 :

 6 Fig. 6: The differences based on the level of education.

Fig. 7 :

 7 Fig. 7: Differences based on years of experience.

Fig. 8 :

 8 Fig. 8: Differences based on working sector.

TABLE I :

 I DIMENSION MEASUREMENT

	Exertion Dimension	Measurement

Physical

Transfer a Bedridden patient from a hospital bed onto a CT table Prepare the examination room for receiving next patient Prepare and administrate for contrast media Mental working in an understaffed environment the department needs more CT Scan machine the management targets are unreasonable

ACKNOWLEDGMENT

The authors thank the Ministry of Health of Saudi Arabia for granting ethical approval and access to its facilities and employees. Special thanks go to Khaled Mohammed Al-Moadi for proving the images presented in this study.


Neil Ayeb

Eric Rutten

Sebastien Bolle

Thierry Coupaye

Marc Douet

Towards an autonomic and distributed device management for the Internet of Things

Keywords: autonomic computing, device management, firmware update, configuration, distribution, internet of things

Device Management (DM) is currently industrially deployed for LAN devices, phones and workstation management. Internet of Things (IoT) devices are massive, dynamic, heterogeneous, and inter-operable. Existing solutions are not suitable for IoT management. This doctoral research in an industrial environment addresses these limitations with a novel autonomic and distributed approach for the DM.

I. CONTEXT AND MOTIVATION

A. Motivation: DM for the IoT

ABIResearch affirm that Device Management (DM) of the Internet of Things (IoT) will grow to US$20.5 Billion by 2023 [START_REF]IoT Device Management Revenues to Climb to US$20.5 Billion by 2023[END_REF]. DM consists of remote and potentially massive operations on a fleet of deployed devices (e.g., home gateways, Set-topboxes, IoT gateways, sensors ...). It is currently massively used by Internet Service Providers (ISP) for LAN devices management and industrials for smartphones and workstations management.

Main features of DM are the following

• Provisioning: initial and 'in-life' setup and configuration • Monitoring: probe data pushing • Assistance: remote troubleshoot • Maintenance: firmware updates IoT relies on massive deployment of connected devices. This implies several constraints such as high number of devices, heterogeneity their types and capabilities and dynamic environments. Challenges emerge from IoT DM:

• Heterogeneity: Current use-cases are targeting a small and fixed set of device types. For instance, ISPs usually manage consumer premises equipments (CPE) such as home gateways and set-top-boxes. IoT implies that numerous device types will be dynamically managed by multiple actors (owners or users). [START_REF] Gartner | [END_REF] implies a significant increase of monitoring data sent to the DM platform. Thus distributing these will allow more efficient network usage and lower reaction times to errors or alerts.

B. Limitations

1) Classical DM solutions limitations: Administrators, industrials, and service providers resort to various DM solutions depending on their device target. ISP's and LAN device manufacturers tend to use TR-069 based DM platforms such as GenieACS [START_REF]GenieACS[END_REF], FreeACS [START_REF]Freeacs[END_REF] or internally developed solutions.

Industrials utilizes Mobile Device Management solutions [3] [4] and workstation administration tools to remotely manage their device fleets (phones, tablets, servers, workstations...). For instance, Microsoft System Configuration Manager [START_REF]Microsoft System Center Configuration Manager[END_REF] allows the aforementioned devices to be managed via a single, yet closed, non-standardized and mono-actor platform.

These solutions rely on manual configuration and driving by a system administrator. Experience reports from industrials shows that even with a small and fixed set of device types, these solutions are complex to operate.

2) Industrial IoT platforms DM limitations: Commercial IoT platforms such as AWS IoT [START_REF]AWS IoT Device Management Documentation[END_REF], Azure IoT Hub [START_REF]Azure IoT Hub Documentation -Tutorials, API Reference[END_REF], or Orange Live Objects [START_REF]Orange Live Objects[END_REF] claim to be able to execute an operation on a massive float of devices with conditions on their state (values of their data-model). Actions targets and conditions are still managed by the administrator via a platform-wide dashboard. To the extent of our knowledge, these commercial platforms do not include an operation model allowing granular tracking of the execution. Such mechanisms would help (in case of operation failure) identifying what step failed and aborting operations on pending and on-going devices.

Current industrial solutions are centralized and designed to manage a small and static set of devices. These solutions are driven by a single actor's administrator. With IoT's challenges (i.e., heterogeneity, dynamicity, interoperability, scalability) complexity will be challenging system administrators making them less efficient in DM solutions configuration and operation. Moreover, centralized designs are not adequate to manage massive remote DM operations and their granular tracking.

II. OBJECTIVES & CONTRIBUTION

A. Objectives 1) Automation: In order to tackle complexity challenge, automation is used as a means of abstracting a system's granular functioning details and system initiated action triggering. Autonomic Computing (AC) is defined by [START_REF] Kephart | The vision of autonomic computing[END_REF] as the selfmanagement capabilities of a system. AC purpose is addressing the increasing complexity of the system administration. An autonomic system can react and adapt to external and internal changes by reconfiguring itself. This behavior has been traditionally within the responsibilities of the system administrator. AC allows to reduce the complexity of system management via less interactions with the administrator and complexity abstraction. The autonomic of a system is enabled via autonomic managers dispatching and coordination [START_REF] Weyns | On Patterns for Decentralized Control in Self-Adaptive Systems[END_REF] [START_REF] Al-Shishtawy | A Design Methodology for Self-Management in Distributed Environments[END_REF].

2) Distribution: In order to tackle the scalability issues of the static and centralized design of currently used DM solutions, it is aimed to dynamically distribute the platform and its managing system. Such design allows more efficient usage of the infrastructure (network, computing and memory capabilities). For instance, monitoring data will be pushed to a geographically close node instead of the existing cloud hosted storage. Besides, having parts of the DM platform closer to managed devices allow better reactivity, higher privacy, and enhanced troubleshooting.

B. Contribution

1) Originality: DM Platforms are not designed with the IoT in mind. Main solutions target LAN devices, phones or workstations. Even though IoT Platforms (e.g., Azure, AWS, Live Objects) include a DM module, they are centralized and manually configured. Distribution for the IoT is mainly about data and services are rarely tackles DM challenges.

2) Adequacy: In order to address the complexity brought by heterogeneity, automation seems adequate. For dynamicity, loop-based control and automation is identified. Interoperability is tackled with model-based aspect of DM automation. Scalability is treated via distribution.

III. METHODOLOGY & EARLY RESULTS

A. Methodology 1) Operation automation and tracking: This loops objective is to keep the fleet up to date, potentially considering interdependencies between devices. It consists of monitoring the device fleet states (i.e., internal and external environments), then computing if DM operations are required. An administrator still can manually trigger these operations. Then it reschedules or modifies the pending or on-going operations if needed. Finally, it keeps tracking the execution of the pushed operations for error management policies enforcement (e.g., stop applying a faulty operation, rollback, alert triggering). The control loop can be operating at a fixed frequency (using parameters such as: amount of on-going operations, fleet size, device type...) or event-triggered.

Via this autonomic manager, the DM platform is going towards self-operation and self-healing. Indeed, beside the traditional configuration by the administrator, the platform can trigger DM operations in an autonomous manner. It is also able to track operations and react to errors unlike existing designs where error detection and reaction is not fully automated and tracking manually realized by the administrator.

2) DM platform and control resource usage regulation: This loops objective is to scale up and down depending on high level objectives and load. It monitors the infrastructure used to operate the DM platform and its autonomic managers (e.g., network load, hops, memory and CPU usage). Based on KPIs received from the platform administrator, reconfiguration will be considered and if needed applied. Actual enforcement of the reconfiguration plan is executed via DM servers (de)instantiation or control loops distribution or centralization. For this manager we will consider model-based appraoches, related to application of control theory [START_REF] Litoiu | What Can Control Theory Teach Us About Assurances in Self-Adaptive Software Systems?[END_REF].

3) Multi-loop coordination and distribution: The two identified managers need interaction and coordination either via a higher global manager (hierarchical) or via direct connection (e.g., master/slave, local coordination, shared elements) [START_REF] Weyns | On Patterns for Decentralized Control in Self-Adaptive Systems[END_REF] [14] [START_REF] Sylla | Design Framework for Reliable Multiple Autonomic Loops in Smart Environments[END_REF].

B. Early results

A first proof-of-concept that has been implemented and is composed of the following entities:

• Two DM Clients (representing two devices) with different battery level and firmware version. • A single DM Server that manages both devices.

• An autonomic manager which manages the DM platform. For the implementation, we used Python [START_REF]Python Software Foundation[END_REF] for the autonomic loop design and the open-source project Eclipse Leshan [START_REF]Eclipse Leshan[END_REF] that we modified for the client and the server.

Leshan project is a Java implementation of an OMA LightWeight M2M [START_REF] Lightweight | [END_REF] DM Protocol, client and server (among other components). The LWM2M Client has been modified to simulate a charging device and an always pluggedin device.

A device that is compliant (state-wise) to a pushed operation condition will be updated, while the other will stay on a 'pending' state until compliance or operation expiry.

IV. FUTURE WORK

Next steps consists of multiple decentralized DM instance and distributed control and current loop elaboration and interaction. Besides, modeling work is currently on-going to achieve model-based control [START_REF] Litoiu | What Can Control Theory Teach Us About Assurances in Self-Adaptive Software Systems?[END_REF]. This will allow interoperability, granular DM operation tracking and troubleshooting, and scalability. Distribution criteria (e.g., geoloc, topology, load...) will also be studied.


Frédéric Lang

Radu Mateescu

Franco Mazzanti

Compositional Verification of Concurrent Systems by Combining Bisimulations

One approach to verify a property expressed as a modal µcalculus formula on a system with several concurrent processes is to build the underlying state space compositionally (i.e., by minimizing and recomposing the state spaces of individual processes, keeping visible only the relevant actions occurring in the formula), and check the formula on the resulting state space. It was shown previously that, when checking the formulas of the L dsbr µ fragment of µ-calculus (consisting of weak modalities only), individual processes can be minimized modulo divergencepreserving branching (divbranching) bisimilation. In this paper, we refine this approach to handle formulas containing both strong and weak modalities, so as to enable a combined use of strong or divbranching bisimulation minimization on concurrent processes depending whether they contain or not the actions occurring in the strong modalities of the formula. We extend L dsbr µ with strong modalities and show that the combined minimization approach preserves the truth value of formulas of the extended fragment. We implemented this approach on top of the CADP verification toolbox and demonstrated how it improves the capabilities of compositional verification on realistic examples of concurrent systems.

Introduction

We consider the problem of verifying a temporal logic property on a concurrent system P 1 || ... || P n consisting of n processes composed in parallel. We work in the action-based setting, the property being specified as a formula ϕ of the modal µ-calculus (L µ ) [START_REF] Kozen | Results on the Propositional µ-calculus[END_REF] and the processes P i being described in a language with process algebraic flavour. A well-known problem is the state-space explosion that happens when the system state space exceeds the available computer memory.

Compositional verification is a set of techniques and tools that have proven efficient to palliate state-space explosion in many situations [START_REF] Garavel | Compositional Verification of Asynchronous Concurrent Systems Using CADP[END_REF]. These techniques may be either independent of the property, i.e., focus only on the construction of the system state space, such as compositional state space construction [START_REF] Malhotra | A Tool for Hierarchical Design and Simulation of Concurrent Systems[END_REF][START_REF] Krishan | An Algorithmic Procedure for Checking Safety Properties of Protocols[END_REF][START_REF] Kuo | Hierarchy-Based Incremental Reachability Analysis of Communication Protocols[END_REF][START_REF] Kuo | An Incremental Approach to Reachability Analysis of Distributed Programs[END_REF][START_REF] Graf | Compositional Minimization of Finite State Systems[END_REF][START_REF] Valmari | Compositional State Space Generation[END_REF][START_REF] Krimm | Compositional State Space Generation from LOTOS Programs[END_REF]. Alternatively, they may depend on the property, e.g., verification of the property on the full system is decomposed in the verification of properties on (expectedly smaller) sub-systems, such as in compositional reachability analysis [START_REF] Wei | Compositional Reachability Analysis Using Process Algebra[END_REF][START_REF] Cheung | Enhancing Compositional Reachability Analysis with Context Constraints[END_REF], assume-guarantee reasoning [START_REF] Pnueli | In Transition from Global to Modular Temporal Reasoning about Programs[END_REF], or partial model checking [START_REF] Reif | Partial Model Checking[END_REF].

Nevertheless, the frontier between property-independent and property-dependent techniques is loose. In compositional state space construction, to be able to reduce the system size, a set of actions is selected and a suitable equivalence relation (e.g., strong bisimulation, branching bisimulation, or divergence-preserving branching bisimulation -divbranching for short) is chosen, restricting the set of properties preserved after hiding the selected actions and reducing the system w.r.t. the selected relation. Therefore, there is still a dependency between the state space construction and the set of properties that can be verified. Given a formula ϕ of L µ to be verified on the system, Mateescu & Wijs [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF] have pushed this idea and shown how to extract a maximal hiding set of actions and an equivalence relation (either strong or divbranching bisimulation) automatically from ϕ, thus inviting the compositional state space construction technique to the table of property-dependent reductions. To select the equivalence relation from the formula, they have identified an L µ fragment named L dsbr µ , which is adequate with divbranching bisimulation [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF]. This fragment consists of L µ restricted to weak modalities, which match actions preceded by arbitrary sequences of hidden actions, as opposed to traditional strong modalities α ϕ 0 and [α] ϕ 0 , which match only a single action satisfying α. If ϕ belongs to L dsbr µ , then the system can be reduced for divbranching bisimulation; otherwise, it can be reduced for strong bisimulation, the weakest equivalence relation preserving full L µ .

In this paper, we revisit and refine this approach to accommodate L µ formulas containing both strong and weak modalities. To do so, we define a logic named L strong µ (A s ), which extends L dsbr µ with strong modalities matching only the actions belonging to a given set A s of strong actions. The set A s induces a partition of the processes P 1 || ... || P n into those containing at least one strong action, and those that do not. We show that a formula ϕ of L strong µ (A s ) is still preserved if the processes containing strong actions are reduced modulo strong bisimulation and the other ones modulo divbranching bisimulation. We also provide guidelines for extracting the set A s from particular L µ formulas encoding the operators of widely-used temporal logics, such as CTL [START_REF] Clarke | Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications[END_REF], ACTL [START_REF] De Nicola | Action versus State Based Logics for Transition Systems[END_REF], PDL [START_REF] Michael | Propositional Dynamic Logic of Regular Programs[END_REF], and PDL-∆ [START_REF] Streett | Propositional Dynamic Logic of Looping and Converse[END_REF]. This combined use of bisimulations to reduce different parts of the same system makes possible a fine-tuning of the compositional state space construction by going smoothly from strong bisimulation (when all modalities are strong) to divbranching bisimulation (when A s is empty, as in the previous approach based on L dsbr µ ). We implemented this approach on top of the CADP verification toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF], and demonstrated how it improves the capabilities of compositional verification on two realistic case studies, namely the TFTP plane-ground communication protocol specified in [START_REF] Garavel | Verification of GALS Systems by Combining Synchronous Languages and Process Calculi[END_REF] and the parallel CTL benchmark of the RERS'2018 challenge.

The paper is organized as follows. Section 2 recalls some definitions. Section 3 defines L strong µ (A s ) and proves the main result of its adequacy with the combined use of strong and divbranching bisimulations. Section 4 presents the experimental results obtained on the two case studies. Finally, Section 5 contains concluding remarks and directions of future work. Formal proofs and code of case studies are available at http://doi.org/10.5281/zenodo.2634148.

Background

LTS compositions and reductions

We consider systems whose behavioural semantics can be represented using an LTS (Labelled Transition System).

Definition 1 (LTS).

Let A denote an infinite set of actions, including the invisible action τ , which denotes internal behaviour. All other actions are called visible. An LTS is a tuple (Σ, A, -→, p init ), where Σ is a set of states, A ⊆ A is a set of actions, -→ ⊆ Σ × A × Σ is the (labelled) transition relation, and

p init ∈ Σ is the initial state. We write p a -→ p if (p, a, p ) ∈ -→ and p τ * -→ p
if there is a (possibly empty) sequence of τ -transitions from p to p , i.e., states p 0 , . . . , p n (n ≥ 0) such that p = p 0 , p = p n , and p i τ -→ p i+1 for i = 0, . . . , n-1.

LTS can be composed in parallel and their actions can be abstracted away using the parallel composition and hiding operators defined below. Prior to hiding, an action mapping operator is also introduced for the generality of the approach.

Definition 2 (Parallel composition of LTS). Let P = (Σ P , A P , -→ P , p init ),

Q = (Σ Q , A Q , -→ Q , q init ), and A sync ⊆ A \ {τ }. The parallel composition of P and Q with synchronization on A sync , "P |[A sync ]| Q", is defined as (Σ P × Σ Q , A P ∪ A Q , -→, (p init , q init ))
, where (p, q) a -→ (p , q ) if and only if either (1) p a -→ p , q = q, and a / ∈ A sync , or (2) p = p, q a -→ q , and a / ∈ A sync , or (3) p a -→ p , q a -→ q , and a ∈ A sync . Definition 3 (Action mapping). Let P = (Σ P , A P , -→ P , p init ) and a total function ρ : A P → 2 A . We write ρ(A P ) for the image of ρ, defined by a∈A P ρ(a). We write ρ(P ) for the action mapping ρ applied to P , defined as the LTS (Σ P , ρ(A P ), -→ P , p init ) where

-→ P = {(p, a , p ) | p a -→ P p ∧ a ∈ ρ(a)}. An action mapping ρ is admissible if τ ∈ A P =⇒ ρ(τ ) = {τ }.
Action mapping enables a single action a to be mapped onto the empty set of actions, onto a single action a , or onto more than one actions a 0 , . . . , a n+1 (n ≥ 0). In the first case, every transition labelled by a is removed. In the second case, a is renamed into a . In the third case, every transition labelled by a is replaced by n + 2 transitions with same source and target states, labelled by a 0 , . . . , a n+1 . Action hiding is a special case of admissible action mapping. Definition 4 (Action hiding). Let P = (Σ P , A P , -→ P , p init ) and A ⊆ A \ {τ }. We write "hide A in P " for the LTS ρ(P ), where ρ is the admissible action mapping defined by (∀a

∈ A P ∩ A) ρ(a) = {τ } and (∀a ∈ A P \ A) ρ(a) = {a}.
Parallel composition and admissible action mapping subsume all abstraction and composition operators encodable as networks of LTS [START_REF] Lang | EXP.OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the-fly Verification Methods[END_REF][START_REF] Garavel | Compositional Verification of Asynchronous Concurrent Systems Using CADP[END_REF][START_REF] Sander De Putter | Compositional Model Checking is Lively -Extended Version[END_REF], such as the parallel composition, hiding, renaming, and cut (or restriction) operators of CCS [START_REF] Milner | Communication and Concurrency[END_REF], CSP [START_REF] Brookes | A Theory of Communicating Sequential Processes[END_REF], mCRL [START_REF] Friso | The Syntax and Semantics of µCRL[END_REF], LOTOS [START_REF] Iso/Iec | LOTOS -A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour[END_REF], E-LOTOS [START_REF]ISO/IEC. Enhancements to LOTOS (E-LOTOS)[END_REF], and LNT [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator (Version 6.7)[END_REF], as well as synchronization vectors 3 . In the sequel, we write P 1 || . . . || P n for any expression composing P 1 , . . . , P n using these operators. Given any partition of P 1 , . . . , P n into arbitrary subsets P 1 and P 2 , it is always possible to rewrite P 1 || . . . || P n in the form (|| Pi∈P1 P i ) || (|| Pj ∈P2 P j ), even for non-associative parallel composition operators (e.g., |[. . .]|), using appropriate action mappings 4 .

LTS can be compared and reduced with respect to well-known bisimulation relations. In this paper, we consider strong bisimulation [START_REF] Park | Concurrency and Automata on Infinite Sequences[END_REF] and divbranching bisimulation, which itself derives from branching bisimulation [START_REF] Van Glabbeek | Branching-Time and Abstraction in Bisimulation Semantics[END_REF][START_REF] Van Glabbeek | Branching Time and Abstraction in Bisimulation Semantics[END_REF]. Strong, branching, and divbranching bisimulations are congruences for parallel composition and admissible action mapping. This allows reductions to be applied at any intermediate step during the state space construction, thus potentially reducing the overall cost of reduction. However, since processes may constrain each other by synchronization, composing LTS two by two following the algebraic structure of the composition expression and applying reduction after each composition can be orders of magnitude less efficient than other strategies in terms of the largest intermediate LTS. Finding an optimal strategy is difficult. One generally relies on heuristics to select a subset of LTS to compose at each step of the compositional reduction. In this paper, we will use the smart reduction heuristic [START_REF] Crouzen | Smart Reduction[END_REF][START_REF] Garavel | Compositional Verification of Asynchronous Concurrent Systems Using CADP[END_REF], which is implemented within the SVL [START_REF] Garavel | SVL: a Scripting Language for Compositional Verification[END_REF] tool of CADP [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]. This heuristic tries to find an efficient composition order by analysing the synchronization and hiding structure of the composition expression.

Definition 5 (Bisimulations). A strong bisimulation is a symmetric relation R ⊆ Σ × Σ such that if (p 1 , p 2 ) ∈ R then: for all p 1 a -→ p 1 ,

Temporal logics

Definition 6 (Modal µ-calculus [START_REF] Kozen | Results on the Propositional µ-calculus[END_REF]). The modal µ-calculus (L µ ) is built from action formulas α and state formulas ϕ, whose syntax and semantics w.r.t.

an LTS P = (Σ, A, -→, p init ) are defined as follows:

α ::= a [[a]] A = {a} | false [[false]] A = ∅ | α 1 ∨ α 2 [[α 1 ∨ α 2 ]] A = [[α 1 ]] A ∪ [[α 2 ]] A | ¬α 0 [[¬α 0 ]] A = A \ [[α 0 ]] A ϕ ::= false [[false]] P δ = ∅ | ϕ 1 ∨ ϕ 2 [[ϕ 1 ∨ ϕ 2 ]] P δ = [[ϕ 1 ]] P δ ∪ [[ϕ 2 ]] P δ | ¬ϕ 0 [[¬ϕ 0 ]] P δ = Σ \ [[ϕ 0 ]] P δ | α ϕ 0 [[ α ϕ 0 ]] P δ = {s ∈ Σ | ∃s a -→ s .a ∈ [[α]] A ∧ s ∈ [[ϕ 0 ]] P δ} | X [[X]] P δ = δ(X) | µX.ϕ 0 [[µX.ϕ 0 ]] P δ = k≥0 Φ 0 k P,δ (∅)
where X ∈ X are propositional variables denoting sets of states, δ : X → 2 Σ is a context mapping propositional variables to sets of states, [ ] is the empty context, δ[U/X] is the context identical to δ except for variable X, which is mapped to state set U , the functional Φ 0P,δ : 2 Σ → 2 Σ associated to the formula µX.ϕ 0 is defined as

Φ 0P,δ (U ) = [[ϕ 0 ]] P δ[U/X],
and Φ k means k-fold application. We write

P |= ϕ (read P satisfies ϕ) for p 0 ∈ [[ϕ]] P [ ].
Action formulas α are built from actions and boolean operators. State formulas ϕ are built from boolean operators, the possibility modality α ϕ 0 denoting the states with an outgoing transition labeled by an action satisfying α and leading to a state satisfying ϕ 0 , and the minimal fixed point operator µX.ϕ 0 denoting the least solution of the equation X = ϕ 0 interpreted over 2 Σ . The usual derived operators are defined as follows: boolean connectors true = ¬false and ϕ 1 ∧ ϕ 2 = ¬(¬ϕ 1 ∨ ¬ϕ 2 ); necessity modality [α] ϕ 0 = ¬ α ¬ϕ 0 ; and maximal fixed point operator νX.ϕ 0 = ¬µX.¬ϕ 0 [¬X/X], where ϕ 0 [¬X/X] is the syntactic substitution of X by ¬X in ϕ 0 . Syntactically, and [] have the highest precedence, followed by ∧, then ∨, and finally µ and ν. To have a welldefined semantics, state formulas are syntactically monotonic [START_REF] Kozen | Results on the Propositional µ-calculus[END_REF], i.e., in every subformula µX.ϕ 0 , all occurrences of X in ϕ 0 fall in the scope of an even number of negations. Thus, negations can be eliminated by downward propagation.

Although L µ subsumes most action-based logics, its operators are rather lowlevel and lead to complex formulas. In practice, temporal logics or extensions of L µ with higher-level operators are used, avoiding (or at least reducing) the use of fixed point operators and modalities. We review informally some of these logics (whose operators can be translated to L µ ), which will be useful in the sequel.

Propositional Dynamic Logic with Looping The logic PDL-∆ [START_REF] Streett | Propositional Dynamic Logic of Looping and Converse[END_REF] introduces the modalities β ϕ 0 and β @, where β is a regular formula defined as follows:

β ::= ϕ? | α | β 1 • β 2 | β 1 |β 2 | β * 0
Regular formulas β denote sets of transition sequences in an LTS: the testing operator ϕ? denotes all zero-step sequences consisting of states satisfying ϕ; α denotes all one-step sequences consisting of a transition labeled by an action satisfying α; the concatenation β 1 • β 2 , choice β 1 |β 2 , and transitive-reflexive closure β * 0 operators have their usual semantics transposed to transition sequences. The regular diamond modality β ϕ 0 denotes the states with an outgoing transition sequence satisfying β and leading to a state satisfying ϕ 0 . The infinite looping operator β @ denotes the states having an outgoing transition sequence consisting of an infinite concatenation of subsequences satisfying β.

Action Computation Tree Logic

The logic ACTL\X (ACTL without next operator) [START_REF] De Nicola | Action versus State Based Logics for Transition Systems[END_REF] introduces four temporal operators, whose semantics can be found in terms of L µ formulas in [START_REF] Fantechi | From ACTL to µ-calculus (extended abstract)[END_REF][START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF], where α 1 , α 2 are interpreted over visible actions:

E(ϕ 1 α1 U ϕ 2 ), E(ϕ 1 α1 U α2 ϕ 2 ), A(ϕ 1 α1 U ϕ 2 ), A(ϕ 1 α1 U α2 ϕ 2 )
A transition sequence satisfies the path formula ϕ 1 α1 U α2 ϕ 2 if it contains a visible transition whose action satisfies α 2 and whose target state satisfies ϕ 2 , whereas at any moment before this transition, ϕ 1 holds and all visible actions satisfy α 1 . A sequence satisfies ϕ 1 α1 U ϕ 2 if it contains a state satisfying ϕ 2 and at any moment before, ϕ 1 holds and all visible actions satisfy α 1 . A state satisfies

E(ϕ 1 α1 U α2 ϕ 2 ) (resp. E(ϕ 1 α1 U ϕ 2 )) if it has an outgoing sequence satisfying ϕ 1 α1 U α2 ϕ 2 (resp. ϕ 1 α1 U ϕ 2 ). It satisfies A(ϕ 1 α1 U α2 ϕ 2 ) (resp. A(ϕ 1 α1 U ϕ 2 )) if
all its outgoing sequences satisfy the corresponding path formula. The following abbreviations are often used:

EF α (ϕ 0 ) = E(true true U α ϕ 0 ) AG α (ϕ 0 ) = ¬EF ¬α (true) ∧ ¬E(true true U ¬ϕ 0 )
A state satisfies EF α (ϕ 0 ) if it has an outgoing sequence leading to a transition whose action satisfies α and target state satisfies ϕ 0 . A state satisfies AG α (ϕ 0 ) if none of its outgoing sequences leads to a transition labeled by an action not satisfying α or to a state not satisfying ϕ 0 .

Computation Tree Logic The logic CTL [START_REF] Clarke | Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications[END_REF] contains the following operators:

E(ϕ 1 U ϕ 2 ), A(ϕ 1 U ϕ 2 ), E(ϕ 1 W ϕ 2 ), A(ϕ 1 W ϕ 2 ), EF(ϕ 0 ), AG(ϕ 0 ), AF(ϕ 0 ), EG(ϕ 0 ) A state satisfies E(ϕ 1 U ϕ 2 ) (resp. A(ϕ 1 U ϕ 2 )
) if some of (resp. all) its outgoing sequences lead to states satisfying ϕ 2 after passing only through states satisfying

ϕ 1 . It satisfies E(ϕ 1 W ϕ 2 ) (resp. A(ϕ 1 W ϕ 2 )
) if some of (resp. all) its outgoing sequences either contain only states satisfying ϕ 1 , or lead to states satisfying ϕ 2 after passing only through states satisfying ϕ 1 . A state satisfies EF(ϕ 0 ) (resp. AF(ϕ 0 )) if some of (resp. all) its outgoing sequences lead to states satisfying ϕ 0 . A state satisfies EG(ϕ 0 ) (resp. AG(ϕ 0 )) if some of (resp. all) its outgoing sequences contain only states satisfying ϕ 0 .

Compositional property-dependent LTS reductions

Given a formula ϕ ∈ L µ and a composition of processes P 1 || . . . || P n , [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF] shows two results that allow an LTS equivalent to P 1 || . . . || P n to be reduced compositionally, while preserving the truth value of ϕ. , which is strictly more expressive than µACTL\X 5 and adequate with divbranching bisimulation. This fragment is defined as follows.

Definition 7 (Modal µ-calculus fragment L dsbr µ [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF]). By convention, we use the symbols α τ and α a to denote action formulas such that τ ∈

[[α τ ]] A and τ / ∈ [[α a ]] A . The fragment L dsbr µ
of L µ is defined as the set of formulas that are semantically equivalent to some formula of the following language:

ϕ ::= false | ϕ 1 ∨ ϕ 2 | ¬ϕ 0 | X | µX.ϕ 0 | (ϕ 1 ?.α τ ) * ϕ 2 | (ϕ 1 ?.α τ ) * .ϕ 1 ?.α a ϕ 2 | ϕ 1 ?.α τ @
The ultra-weak modality (ϕ 1 ?.α τ ) * ϕ 2 , weak modality (ϕ 1 ?.α τ ) * .ϕ 1 ?.α a ϕ 2 , and weak infinite looping modality ϕ 1 ?.α τ @ are shorthand notations for the respective L µ formulas µX.ϕ 2 ∨ (ϕ 1 ∧ α τ X), µX.ϕ 1 ∧ ( α a ϕ 2 ∨ α τ X), and νX.ϕ 1 ∧ α τ X. Derived operators are also defined as follows:

[(ϕ 1 ?.α τ ) * ] ϕ 2 = ¬ (ϕ 1 ?.α τ ) * ¬ϕ 2 [ϕ 1 ?.α τ ] = ¬ ϕ 1 ?.α τ @ [(ϕ 1 ?.α τ ) * .ϕ 1 ?.α a ] ϕ 2 = ¬ (ϕ 1 ?.α τ ) * .ϕ 1 ?.α a ¬ϕ 2
Depending on the L µ fragment ϕ belongs to, it is thus possible to determine whether the system can or cannot be reduced for divbranching bisimulation.

P = p0 a 1 / / p1 τ b b Q = q0 a 1 / / q1 τ / / q2 a 2 g g P = p 0 a 1 x x Q = q 0 a 1 / / q 1 a 2 b b P |[a1]| Q = (p0, q0) a 1 / / (p1, q1) τ / / τ (p1, q2) a 2 / / τ (p1, q0) τ v v (p0, q1) τ / / (p0, q2) a 2 V V

Applying divbranching bisimulation to selected components

The following theorem states the main result of this paper, namely that every component process containing no strong action can be replaced by any divbranching equivalent process, without affecting the truth value of the formula6 .

Theorem 2. Let P = (Σ P , A P ,

→ P , p init ), Q = (Σ Q , A Q , -→ Q , q init ), Q = (Σ Q , A Q , -→ Q , q init ), A sync ⊆ A, and ϕ ∈ L strong µ (A s ). If A Q ∩ A s = ∅ and Q ∼ dsbr Q , then P |[A sync ]| Q |= ϕ if and only if P |[A sync ]| Q |= ϕ.
Proof. The proof looks like the one in [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF], showing that divbranching bisimulation preserves the properties of L dsbr µ , but reasoning concerns product states and additionally handles the case of strong modalities.

Note that τ may belong to A s . If so, every P i containing τ cannot be reduced for divbranching bisimulation. On the contrary, processes that do not contain strong actions do not contain τ . Reducing them for divbranching bisimulation is thus allowed, but coincides with strong bisimulation reduction. In the end, all τ -transitions of the system are preserved, as expected for the truth value of formulas containing strong modalities matching τ to be preserved.

Example 2. In Example 1, P does not contain a 2 , the only strong action of the system. Thus, ϕ can be checked on P |[a 1 ]| Q (which is isomorphic to Q and has only 3 states) instead of P |[a 1 ]| Q (6 states), while preserving its truth value.

Theorem 2 is consistent with Andersen's partial model checking [START_REF] Reif | Partial Model Checking[END_REF] and the mono-bisimulation approach [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF]. Given P || Q such that the strong actions of ϕ occur only in P , one can observe that the quotient ϕ//P (defined in [START_REF] Reif | Partial Model Checking[END_REF][START_REF] Lang | Partial Model Checking using Networks of Labelled Transition Systems and Boolean Equation Systems[END_REF]) belongs to L dsbr µ , because quotienting removes all strong modalities, leaving only weak modalities in the quotiented formula. It follows that Q, on which ϕ//P has to be checked, can be reduced for divbranching bisimulation. This observation could serve as an alternative proof of Theorem 2.

Identifying strong actions in derived operators

In the general case, identifying a minimal set of strong actions is not easy, if even feasible. One cannot reasonably assume that formulas are written in the obscure L strong µ (A s ) syntax (see Ex. 1) and that the remaining strong modalities cannot be turned to weak ones. Instead, users shall continue to use "syntactic sugar" extensions of L µ , with operators of e.g., CTL, ACTL, PDL, or PDL-∆. In Lemma 1, we provide patterns that can be used to prove that a formula written using one of those operators belongs to a particular instance of

L strong µ (A s ). Lemma 1. Let ϕ 0 , ϕ 1 , ϕ 2 ∈ L strong µ (A s ), τ ∈ [[α τ ]] A , τ / ∈ [[α a ]] A , [[α s ]] A ⊆ A s ,
and α 0 , α 1 , α 2 be any action formulas. The following formulas belong to L strong µ (A s ) (the list may be not exhaustive):

1. Modal µ-calculus:

α s ϕ 0 [α s ] ϕ 0 ¬ϕ 0 ϕ 1 ∨ ϕ 2 ϕ 1 ∧ ϕ 2 ϕ 1 ⇒ ϕ 2 2. Propositional Dynamic Logic: α * τ ϕ 0 [α * τ ] ϕ 0 α * τ • α a ϕ 0 [α * τ • α a ] ϕ 0 α τ @ [α τ ] 3. Action Computation Tree Logic: A(ϕ 1 α1 U ϕ 2 ) A(ϕ 1 α1 U α2 ϕ 2 ) AG α0 (ϕ 0 ) E(ϕ 1 α1 U ϕ 2 ) E(ϕ 1 α1 U α2 ϕ 2 ) EF α0 (ϕ 0 ) 4. Computation Tree Logic: A(ϕ 1 U ϕ 2 ) A(ϕ 1 W ϕ 2 ) AG(ϕ 0 ) AF(ϕ 0 ) E(ϕ 1 U ϕ 2 ) E(ϕ 1 W ϕ 2 ) EF(ϕ 0 ) EG(ϕ 0 ) A([α a ] ϕ 1 U ϕ 2 ) A([α a ] ϕ 1 W ϕ 2 ) AG([α a ] ϕ 0 ) EF( α a ϕ 0 ) AG(ϕ 1 ∨ [α a ] ϕ 2 ) EF(ϕ 1 ∧ α a ϕ 2 )
Example 3. Let a 1 , a 2 , and a 3 be visible actions and recall that A denotes the set of all actions of the system. Lemma 1 allows the following to be shown (this is left as an exercise):

true * .a 1 .(¬a 2 ) * .a 3 true ∈ L strong µ (∅) [true] false ∈ L strong µ (A) A( a 1 true ¬a2 U a3 true) ∈ L strong µ ({a 1 }) AG([a 1 ] false) ∈ L strong µ (∅) E(true true U τ true) ∈ L strong µ (A) a * 1 .a 2 true ∈ L strong µ ({a 1 , a 2 }) E(true true U τ true) ∈ L strong µ ({τ }) [a 1 .a 2 ] false ∈ L strong µ ({a 1 , a 2 }) EF( a 1 true ∧ a 2 true) ∈ L strong µ ({a 1 }) EF( a 1 a 2 true) ∈ L strong µ ({a 2 }) EF( a 1 true ∧ a 2 true) ∈ L strong µ ({a 2 }) EF( ¬a 1 true) ∈ L strong µ (A \ {a 1 })
Theorem 3. There is not a unique minimal set A s such that ϕ ∈ L strong µ (A s ).

Proof. EF( a 1 true ∧ a 2 true) ∈ L strong µ ({a 1 }) ∩ L strong µ ({a 2 }), because it is semantically equivalent to both formulas EF( ( a 1 true?.true) * . a 1 true?.a 2 true) and EF( ( a 2 true?.true) * . a 2 true?.a 1 true). Yet, it is not in L strong µ (∅) as it has not the same truth value on the divbranching equivalent LTS P and P below:

P = p0 a 1 a 2 < < τ $ $ p1 P = q0 a 1 / / τ ' ' q1 q2 a 2 o o τ g g
Thus, {a 1 } and {a 2 } are non-unique minimal sets of strong actions.

Applications

We consider two examples to illustrate our new verification approach combining strong and divbranching bisimulation and show how it can reduce both time and memory usage when associated to the smart reduction heuristic. In both examples, the aim is to perform a set of verification tasks, each consisting in checking a formula ϕ on a system of parallel processes P 1 || . . . || P n . Since our approach can only improve the verification of formulas containing both strong and weak modalities, we consider only the pairs of formulas and systems such that the formula is part of L strong µ (A s ) for some minimal A s that is not empty and that is strictly included in the set of visible actions of the system7 . For each verification task, we compare the largest LTS size, the verification time, and the memory peak obtained using the following two approaches: All experiments were done on a 3GHz/12GB RAM/8-core Intel Xeon computer running Linux, using the specification languages and 32-bit versions of tools provided in the CADP toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] version 2019-a "Pisa".

Mono-

Trivial File Transfer Protocol

The TFTP (Trivial File Transfer Protocol ) case-study8 addresses the verification of an avionic communication protocol between a plane and the ground [START_REF] Garavel | Verification of GALS Systems by Combining Synchronous Languages and Process Calculi[END_REF].

It comprises two instances (A and B) of a process named TFTP, connected through a FIFO buffer. Since the state space is very large in the general case, the authors defined five scenarios named A, B, C, D, and E, depending on whether each instance may write and/or read a file. The system corresponding to each scenario is a parallel composition of eight processes. The requirements consist of 29 properties parameterized by the identity of a TFTP instance, defined in MCL [START_REF] Mateescu | A Model Checking Language for Concurrent Value-Passing Systems[END_REF] (an implementation of the alternation-free modal µ-calculus including PDL-∆ modalities and macro definitions enabling the construction of libraries of operators), 24 of which belong to L dsbr µ . The remaining five, namely properties 08, 09, 14, 16, and 17, contain both weak and strong modalities. The shape of these properties is described in Table 1, where we do not provide the details of the action formulas, but instead denote them by letters a 1 , a 2 , . . ., where τ for all i. Strong action formulas are highlighted and one shows easily that the other are weak using Lemma 1-2.

/ ∈ [[a i ]] A Nr. Property 08 [true * • a1 • a2] false 09 [true * • a1 • a2 • ((a3 • (¬a4) * • a5)|(a6 • (¬a7) * • a8))] false 14 [true * • a1 • a2 • (¬a3) * • a4 • a5] false 16 [(¬a1) * • a2 • (¬a3) * • a4] ((¬a5) * • a6 • a7) • ((¬a5)
We consider 31 among a potential of 50 verification tasks (five properties, five scenarios, and two instances) as some properties are not relevant to every TFTP instance and scenario (e.g., in a scenario where one TFTP instance only receives messages, checking a property concerning a message emission is irrelevant). All 31 verification tasks return true and the strong actions occur in only three (although not the same three) out of the eight parallel processes.

Fig. 2. Experimental results of the TFTP case-study

Figure 2 shows that the refined approach always reduces LTS size (for both intermediate and final LTS), memory and time following similar curves, up to a factor 7 (the vertical axis is on a logarithmic scale). Time does not include LTS generation of the component processes from their LNT specification, which takes only a few seconds and is common to both approaches. In these experiments, time is dominated by the last step of generation and minimization, whereas memory usage is dominated by minimization.

[A11] A([A2] false W A6 true) ⇒ [A11] A([A5] false W A6 true)) true 103#22 EG([A14] false ∧ ( A18 true ⇒ [A18] EG([A21] false ∧ EF( A19 true)))) true = EG([A14] false ∧ [A18] EG([A21] false ∧ EF( A19 true))) 103#23 AG( A34 true ⇒ [A34] A([A68] false W A59 true)) false = AG([A34] A([A68] false W A59 true))

Parallel benchmark of the RERS 2018 challenge

The RERS (Rigorous Examination of Reactive Systems) 9 challenge is an international competition on a benchmark of verification tasks. Since 2018 (8th edition), the challenge features a set of parallel problems where systems are synchronizing LTS and properties are expressed using CTL and modalities. This section illustrates the benefits of our approach on these problems.

The benchmark comprises three specifications of concurrent systems, numbered 101, 102, and 103, each accompanied by three properties to be checked, numbered p#21, p#22, and p#23, where p is the system number. Thus, nine verification tasks have to be solved. The properties are presented in Table 2, where the strong action formulas are highlighted. One easily shows that all other action formulas are weak using Lemmas 1-1 and 1-4. However, for 103#22 and 103#23, the identity (

α true ⇒ [α] ϕ) = ([α] false ∨ [α] ϕ) = [α] ϕ (because [α] false =⇒ [α]
ϕ for all ϕ) was applied to obtain the simplified formulas occurring after the = sign in the table. For 102#23, this simplification allowed us to prove that A34 is not a strong action, unlike what appears at first sight.

Table 3 gives, for each of the nine verification tasks, the number #act of actions in the system, the number #hide of actions in the maximal hiding set, the number #sact of strong actions, the number #proc of parallel processes, the number #sproc of processes in the strong group, the number #sync of intergroup actions, and the best reduction relation among strong bisimulation, divbranching bisimulation, or a combination of both. We observe that:

-The set of weak actions of 101#21 is empty due to the presence of the "true" strong action formula, whereas the set of strong actions of 102#21 is empty, i.e., the property belongs to L dsbr µ . In both cases, our approach coincides with the mono-bisimulation approach. The verification of 101#21 (reduced Table 4 compares the performance of verifying the latter seven verification tasks using the approaches described above. LTS sizes are given in kilostates, memory in megabytes, and time in seconds. Tasks using more than 3 GB of memory were aborted. We see that our approach reduces both time and memory usage and allows all problems of the challenge to be solved, whereas using strong bisimulation alone fails in five out of those seven tasks. The negligible reductions in time and memory usage observed for tasks 101#22 and 101#23 are due to the fact that time and memory usage are dominated by the algorithm in charge of selecting a sub-set of processes to be composed and reduced (implemented in smart reduction). The complexity of this algorithm does not depend on the state space size, but on the number of actions and parallel processes, which is almost the same using both approaches. When considering larger examples, memory usage gets dominated by minimisation. In particular, for tasks 102#22, 102#23, 103#21, and 103#23 (and likely also 103#22), memory usage is reduced by several orders of magnitude.

Note that some of these tasks can be verified more efficiently using noncompositional approaches, such as on-the-fly model checking, in cases where proofs or counter-examples can be detected much before having explored the full state space. The main drawback of maximal hiding is that the generated counter-examples are given only in terms of the actions visible in the formula, which abstracts out a lot of intermediate transitions. However, this is the price to pay for being able to verify most of the tasks, such as 103#21, for which on-the-fly verification aborts due to memory exhaustion.

Conclusion and Future Work

In this paper, we proposed a compositional verification approach that extends the state of the art [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF] and consists of three steps: First, so-called strong actions are identified, corresponding to those actions of the system that the formula cannot match using weak modalities in the sense of the L µ fragment L dsbr µ adequate with divbranching bisimulation. These actions are used to partition the parallel processes into those containing strong actions and the others. Second, maximal hiding and compositional reduction are used to minimize the composition of processes not containing strong actions for divbranching bisimulation, and the other processes for strong bisimulation. Finally, the property is verified on the reduced system.

The originality of this approach is to combine strong and divbranching bisimulation, as opposed to the mono-bisimulation approach of [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF]. We proved it correct by characterizing a family of fragments of the logic L µ , called L strong µ (A s ), parameterized by the set A s of strong actions. We also showed under which conditions action-based branching-time temporal logic formulas containing wellknown operators from the logics CTL, ACTL, PDL, and PDL-∆ are part of L strong µ (A s ) when A s is fixed. In the future, it might be worth investigating whether more operators can be considered, e.g., from the linear-time logic LTL.

This approach may significantly improve the verification performance for systems containing both processes with and without strong actions, as illustrated by two case-studies. In particular, it allowed the whole parallel CTL benchmark of the RERS 2018 challenge to be solved on a standard computer.

Identifying (close to minimal) sets of strong actions for arbitrary formulas manually is a cumbersome task, prone to errors. We shall investigate ways to compute such sets automatically. As illustrated by verification task 103#23 of RERS 2018, the problem is not purely syntactic: considering non-trivial semantic equivalences may prove useful to eliminate actions that appear strong at first sight. Yet, we trust that the presented approach has potential to be implemented in automated software tools, such as those available in the CADP toolbox.

A Proof of Theorem 2 (page 9)

To show Theorem 2, we first need the following Lemma, which simply lifts a standard property of branching and divbranching bisimulations up to the level of product states:

Lemma 2. In P |[A sync ]| Q, if (p 0 , q 0 ) a -→ (p 1 , q 1 )
and q 0 ∼ dsbr q 0 then there exists a state q 1 such that q 1 ∼ dsbr q 1 and either:

a = τ , p 0 = p 1 , q 0 ∼ dsbr q 1 , and q 1 = q 0 , or there exists q 0 , ..., q n (n ≥ 0) such that q 0 = q 0 , for all i ∈ 0..n-1, q i+1 ∼ dsbr q 0 , (p 0 , q i ) τ -→ (p 0 , q i+1 ), and (p 0 , q n ) a -→ (p 1 , q 1 ).

Graphically, this means that one of the diagrams below holds, where solid lines denote universal quantification whereas dotted lines denote existential quantification:

(p0, q0)

a=τ / / ∼ dsbr (p1, q1) = ∼ dsbr (p0, q1) (p0, q 0 ) = (p1, q 1 )
-or -

(p0, q0) a / / ∼ dsbr (p1, q1) ∼ dsbr (p0, q 0 ) = (p0, q 0 ) τ / / ∼ dsbr (p0, q 1 ) τ / / ...∼ dsbr ... . . . τ / / (p0, q n ) a / / (p1, q 1 )
Proof. From the definition of P |[A sync ]| Q and the fact that (p 0 , q 0 ) a -→ (p 1 , q 1 ), there are three possible cases:

1. a ∈ A sync , p 0 a -→ p 1 , and q 0 a -→ q 1 , or 2. a / ∈ A sync , p 0 a -→ p 1 , and q 1 = q 0 , or 3. a / ∈ A sync , p 1 = p 0 , and q 0 a -→ q 1

Instead of considering those three cases, we merge cases 1 and 3 (where q 0 a -→ q 1 , whatever p 0 does), which have a similar proof, into a single case. Thus we consider the following two cases, the first one corresponding to case 2 of the above enumeration, and the second one corresponding to cases 1 and 3:

q 1 = q 0 , a /
∈ A sync , and p 0 a -→ p 1 . Take q 1 = q 0 . We have q 1 ∼ dsbr q 1 because q 1 = q 0 , q 0 ∼ dsbr q 0 , and q 0 = q 1 . The second item of the lemma (bottom diagram) is verified with n = 0, q 0 = q n = q 0 , and (p 0 , q 0 ) = (p 0 , q n ) = (p 0 , q 0 ) a -→ (p 1 , q 0 ) = (p 1 , q 1 ).

q 0 a -→ q 1 (and either a / ∈ A sync and p 1 = p 0 , or a ∈ A sync and p 0 a -→ p 1 ). Then since q 0 ∼ dsbr q 0 , we have by definition of ∼ dsbr :

• Either a = τ and q 0 ∼ dsbr q 1 . Since τ / ∈ A sync , we have p 0 = p 1 . Then, we can take q 1 = q 0 . Indeed, q 1 ∼ dsbr q 1 because q 1 = q 0 , q 0 ∼ dsbr q 0 , and q 0 ∼ dsbr q 1 . The first item of the lemma (top diagram) is verified.

• Or there exists q 0 , ..., q n (n ≥ 0) such that q 0 = q 0 , for all i ∈ 0..n -1, q i+1 ∼ dsbr q 0 , q i τ -→ q i+1 , and q n a -→ q 1 . In this case, we also have (p 0 , q i ) τ -→ (p 0 , q i+1 ) and (p 0 , q n ) a -→ (p 1 , q 1 ), i.e., the second item of the lemma (bottom diagram) is verified.

We draw the reader's attention to the fact that the top diagram of Lemma 2 concerns only the case (p 0 , q 0 ) τ -→ (p 0 , q 1 ) deriving from a transition q 0 τ -→ q 1 where q 0 ∼ dsbr q 1 . The bottom diagram concerns all other cases, including (p 0 , q 0 ) τ -→ (p 1 , q 0 ) deriving from p 0 τ -→ p 1 where p 0 ∼ dsbr p 1 . We now show the main theorem:

Theorem 2 Let P = (Σ P , A P , → P , p init ), Q = (Σ Q , A Q , -→ Q , q init ), Q = (Σ Q , A Q , -→ Q , q init ), A sync ⊆ A, and ϕ ∈ L strong µ (A s ). If A Q ∩ A s = ∅ and Q ∼ dsbr Q , then P |[A sync ]| Q |= ϕ if and only if P |[A sync ]| Q |= ϕ.
Proof. We prove that, given p ∈ Σ P , q ∈ Σ Q , and q ∈ Σ Q such that q ∼ dsbr q , (p, q) satisfies ϕ if and only if (p, q ) satisfies ϕ. We show this claim by structural induction on the formula ϕ. Since we work on finite LTS, every formula containing a fixed point operator µ can be expanded into an equivalent formula by unfolding the fixed point a bounded number of times. This way, we do not have to consider fixed points and propositional variables in this proof, and contexts δ mapping propositional variables to sets of states are always empty in the semantics of formulas. For conciseness, we write

[[ϕ]] instead of [[ϕ]] P |[Async ]| Q [ ] and [[ϕ]] P |[Async ]| Q [ ], respectively, as the LTS "P |[A sync ]| Q" or "P |[A sync ]| Q "
to which the semantics apply is clear from the context. Note that since the claim is symmetric, it is sufficient to prove one implication only. We thus assume that (p, q) ∈ [[ϕ]] and prove that (p, q ) ∈ [

[ϕ]]. -Case ϕ = false. It is obvious that both (p, q) / ∈ [[ϕ]] and (p, q ) / ∈ [[ϕ]]. -Case ϕ = ϕ 1 ∨ ϕ 2 . By definition, either (p, q) ∈ [[ϕ 1 ]] or (p, q) ∈ [[ϕ 2 ]]. If (p, q) ∈ [[ϕ 1 ]] (resp. [[ϕ 2 ]]) then (p, q ) ∈ [[ϕ 1 ]] (resp. [[ϕ 2 ]]) by the induction hypothesis. Therefore, (p, q ) ∈ [[ϕ 1 ∨ ϕ 2 ]]. -Case ϕ = ¬ϕ 0 . By definition, (p, q) / ∈ [[ϕ 0 ]]. By the induction hypothesis, (p, q ) / ∈ [[ϕ 0 ]] and thus (p, q ) ∈ [[¬ϕ 0 ]]. -Case ϕ = α s ϕ 0 . By definition, there exists a ∈ [[α s ]] A such that (p, q) a -→ (p 1 , q 1 ) and (p 1 , q 1 ) ∈ [[ϕ 0 ]]. Since [[α s ]] A ⊆ A s , A Q ∩ A s = ∅, and a ∈ [[α s ]] A , we have a /
∈ A Q (and hence, a / ∈ A sync ). Therefore, q = q 1 , p a -→ p 1 , and (p, q ) a -→ (p 1 , q ). Since q ∼ dsbr q and (p 1 , q) ∈ [[ϕ 0 ]], we have by the induction hypothesis

(p 1 , q ) ∈ [[ϕ 0 ]]. As a consequence, (p, q ) ∈ [[ α s ϕ 0 ]]. -Case ϕ = (ϕ 1 ?.α τ ) * ϕ 2 . By definition, there exist m ≥ 0, p i ∈ Σ P , q i ∈ Σ Q , and a i ∈ [[α τ ]] A (i ∈ 0..m), such that (p, q) = (p 0 , q 0 ), (p m , q m ) ∈ [[ϕ 2 ]], and for all 0 ≤ i < m, (p i , q i ) ai -→ (p i+1 , q i+1 ) and (p i , q i ) ∈ [[ϕ 1 ]
]. We show that the same holds from state (p, q ), i.e., there exists a sequence of transitions matching α τ and passing through states satisfying ϕ 1 , until reaching a state satisfying ϕ 2 . By the induction hypothesis, (p, q ) = (p 0 , q 0 ) ∈

[[ϕ 1 ]]. Consider one transition (p i , q i ) ai -→ (p i+1 , q i+1 ). We know that (p i , q i ) ∈ [[ϕ 1 ]
]. Assume that there exists q i ∼ dsbr q i . Substituting a i for a, (p i , q i ) for (p 0 , q 0 ), and (p i+1 , q i+1 ) for (p 1 , q 1 ) in the two diagrams of Lemma 2, it appears clearly that there exists a state q i+1 such that q i+1 ∼ dsbr q i+1 . Moreover, by the induction hypothesis, every state divbranching equivalent to (p i , q i ) in the bottom sequence of the diagrams is in [[ϕ 1 ]]. Finally, note that τ ∈ [[α τ ]] by definition, so that each of the τ -transitions in the bottom sequence of the second diagram thus matches α τ . Moreover, (p m , q m ) ∈ [[ϕ 2 ]] and q m ∼ dsbr q m , so by the induction hypothesis, we have also (p m , q m ) ∈ [[ϕ 2 ]].

-Case ϕ = (ϕ 1 ?.α τ ) * .ϕ 1 ?.α a ϕ 2 . Since (ϕ 1 ?.α τ ) * .ϕ 1 ?.α a ϕ 2 is equivalent to (ϕ 1 ?.α τ ) * (ϕ 1 ?.τ ) * .ϕ 1 ?.α a ϕ 2 and since we have already considered the case ϕ = (ϕ 1 ?.α τ ) * ϕ 2 above, we only have to consider the case ϕ = (ϕ 1 ?.τ ) * .ϕ 1 ?.α a ϕ 2 , i.e., α τ = τ . By definition, there exist m ≥ 0, p i ∈ Σ P , q i ∈ Σ Q (i ∈ 0..m + 1) and a ∈ [[α a ]] A , such that (p, q) = (p 0 , q 0 ), (p m , q m ) a -→ (p m+1 , q m+1 ), (p m+1 , q m+1 ) ∈ [[ϕ 2 ]], and for all 0 ≤ i < m, (p i , q i ) τ -→ (p i+1 , q i+1 ) and (p i , q i ) ∈ [[ϕ 1 ]]. The reasoning is similar to the previous case. It is important to note that the transition (p m , q m ) a -→ (p m+1 , q m+1 ) necessarily has a counterpart in the built sequence, since a ∈ [[α a ]] A and τ / ∈ [[α a ]]. Therefore this transition cannot be an inert transition and the first case of Lemma 2 does not apply here.

-Case ϕ = ϕ 1 ?.α τ @. By definition, there exists an infinite sequence of states (p 0 , q 0 ) a0 -→ (p 1 , q 1 ) a1 -→ . . . (p i , q i ) ai -→ . . ., such that p 0 = p, q 0 = q, and for all i > 0, (p i , q i ) ∈

Example 1 .

 1 Consider the LTS P , P , Q, and Q depicted in Figure 1. P (resp. Q ) denotes the minimal LTS equivalent to P (resp. Q) for divbranching bisimulation. The formula ϕ = [(true?.true) * .true?.a 1 ] [a 2 ] false of L strong µ ({a 2 }) (which is equivalent to the PDL formula [true * .a 1 .a 2 ] false) expresses that the system does not contain two successive transitions labelled by a 1 and a 2 respectively. ϕ does not belong to L dsbr µ . Indeed, P |[a 1 ]| Q satisfies ϕ because a 1 is necessarily followed by a τ transition, but P |[a 1 ]| Q (which is isomorphic to Q ) does not.

Fig. 1 .

 1 Fig. 1. LTS used in Examples 1 and 2

  AG([A21] [A23] [A4] [true] false) false 101#22 AG([A3] AF( A2 true)) false 101#23 AG( A20 true ⇒ A20 A([A23] false W A8 true)) true 102#21 EF(AG([A5] false)) true 102#22 EG([A35] E([A23] false U A35 true)) false 102#23 AG([A22] A([A8] false U A22 true)) false 103#21 AG(

  there exists p 2 such that p 2 a -→ p 2 and (p 1 , p 2 ) ∈ R. A branching bisimulation is a symmetric relation R ⊆ Σ × Σ such that if (p 1 , p 2 ) ∈ R then: for all p 1 Two states p 1 and p 2 are strongly (resp. branching, divbranching) bisimilar, written p 1 ∼ p 2 (resp. p 1 ∼ br p 2 , p 1 ∼ dsbr p 2 ), if there exists a strong (resp. branching, divbranching) bisimulation R such that (p 1 , p 2 ) ∈ R. Two LTS P 1 and P 2 are strongly (resp. branching, divbranching) bisimilar, written P 1 ∼ P 2 (resp. P 1 ∼ br P 2 , P 1 ∼ dsbr P 2 ), if their initial states are strongly (resp. branching, divbranching) bisimilar.

	a = τ and (p 1 , p 2 ) ∈ R, or there exists a sequence p 2	τ * -→ p 2	a -→ p 1 , either -→ p 2 such that a
	(p 1 , p 2 ) ∈ R and (p 1 , p 2 ) ∈ R. A divergence-preserving branching bisimulation
	(divbranching bisimulation for short) is a branching bisimulation R such that if
	(p 0 1 , p 0 2 ) ∈ R and there is an infinite sequence p 0 1 (p i 1 , p 0 2 ) ∈ R for all i ≥ 0, then there is an infinite sequence p 0 τ -→ p 1 1 τ -→ p 2 1 2 τ -→ p 1 -→ . . . with τ 2 τ -→ p 2 τ -→ 2 . . . such that (p i 1 , p j 2 ) ∈ R for all i, j ≥ 0.

  The first result is a procedure, called maximal hiding, which extracts systematically from ϕ a set of actions H(ϕ) that are not discriminated by any action formula occurring in ϕ. It is shown that P 1 || . . . || P n |= ϕ if and only if hide H(ϕ) in (P 1 || . . . || P n ) |= ϕ. The second result is the identification of a fragment of L µ , called L dsbr µ

  bisimulation approach: ϕ is verified on hide H(ϕ) in (P 1 || . . . || P n ) (where H(ϕ) is the maximal hiding set mentioned in Sect. 2.3) reduced compositionally for strong bisimulation (since ϕ is not in L dsbr The set {P 1 , . . . , P n } is partitioned in two groups P s and P w such that P i ∈ P s if it contains actions in A s and P i ∈ P w otherwise, so that P 1 || . . . || P n can be rewritten in the equivalent form (|| Pi∈Ps P i ) || (|| Pj ∈Pw P j ). The set A I of actions on which at least one process of P s and one process of P

	µ	) using the
	smart reduction heuristic.
	Refined approach combining bisimulations:

w synchronize (intergroup synchronization) is then identified. Using the smart reduction heuristic, hide H(ϕ) \ A I in || Pi∈Ps P i (corresponding to the processes containing strong actions) is reduced compositionally for strong bisimulation, leading to a first LTS P s , and hide H(ϕ) \ A I in || Pj ∈Pw P j (corresponding to the processes containing no strong action) is reduced compositionally for divbranching bisimulation, leading to a second LTS P w . Finally, ϕ is verified on hide H(ϕ) ∩ A I in (P s |[A I ]| P w ) reduced for strong bisimulation.

Table 1 .

 1 • a6 • a7) true 17 Same shape as property Nr. 16 TFTP properties (strong action formulas are highlighted)

*

Table 2 .

 2 RERS 2018 properties (strong action formulas are highlighted)

Table 3 .

 3 Some numbers about the RERS 2018 parallel benchmark for strong bisimulation) takes 75 seconds, with a memory peak of 11 MB and a largest LTS of 83, 964 states and 374, 809 transitions. The verification of 102#21 (reduced for divbranching bisimulation) takes 261 seconds, with a memory peak of 22 MB and a largest LTS of 243 states and 975 transitions. -101#22, 101#23, 102#22, 102#23, 103#21, 103#22, and 103#23 contain both weak and strong actions. They are used to evaluate our approach.

	Task #act #hide #sact #proc #sproc #sync	relation
	101#21 24	21	24	9	9	-	strong
	101#22 24	22	1	9	4	11	combination
	101#23 24	21	2	9	3	9	combination
	102#21 28	27	0	20	0	-	divbranching
	102#22 28	26	2	20	10	14	combination
	102#23 28	26	1	20	4	12	combination
	103#21 70	66	2	34	8	12	combination
	103#22 70	66	3	34	6	18	combination
	103#23 70	67	1	34	7	10	combination

Table 4 .

 4 Experimental results of the RERS 2018 parallel benchmark

		Strong bisimulation Combined bisimulations
		Kstates	verif.	Kstates	verif.
	Task largest final MB sec. largest final MB sec.
	101#22	84	77 10 77	1.4	1.4	10 72
	101#23	84	77 11 80	0.5	0.5	8	73
	102#22	-	-	-	-	611	585 57 295
	102#23	-	-	-	-	17	9.8	22 260
	103#21	-	-	-	-	734	313 101 604
	103#22	-	-	-	-14,143 14,141 1575 2533
	103#23	-	-	-	-	122	122 35 566

Table 5 .

 5 [[ϕ 1 ]] and a i ∈ [[α τ ]].The reasoning is similar Results of the TFTP case-study

	Strong bisimulation Combined bisimulations Ratio Strong/Combined
	Kstates	verif.	Kstates	verif.	Kstates	verif.
	P S I largest final MB sec. largest final MB sec. largest final MB sec.
	08 A A 1783 1197 136 66	746	503 60 32	2.4 2.4 2.3 2.1
	14 A A 1783 1495 138 83	770	639 62 31	2.3 2.3 2.2 2.7
	08 A B 1783 1295 143 91	347	281 30 17	5.1 4.6 4.8 5.4
	17 A B 1783 1191 138 76	1000 694 79 44	1.8 1.7 1.7 1.7
	08 B A 792	636 62 38	347	289 30 18	2.3 2.2 2.1 2.1
	08 B B 792	707 62 40	174	130 17 13	4.6 5.4 3.6 3.1
	14 B B 792	720 65 47	174	134 17 14	4.6 5.4 3.8 3.4
	16 B B 792	613 63 35	456	356 38 22	1.7 1.7 1.7 1.6
	08 C A 30926 16924 2393 2274 8448 4471 660 575	3.7 3.8 3.4 4.0
	09 C A 30965 16935 2540 2305 7940 7516 636 666	3.9 2.3 4.0 3.5
	14 C A 30965 22772 2417 3033 8679 6141 688 706	3.6 3.7 3.5 4.3
	17 C A 30992 16935 2527 1873 19269 10833 1502 1164 1.6 1.6 1.7 1.6
	08 C B 30926 16853 2391 2257 7995 4176 617 417	3.9 4.0 3.9 5.4
	09 C B 30953 16998 2538 2271 7326 6931 589 502	4.2 2.5 4.3 4.5
	14 C B 30953 22710 2410 2635 8146 5683 637 601	3.8 4.0 3.8 4.4
	17 C B 30992 16998 2529 1913 18033 10173 1406 1155 1.7 1.7 1.8 1.7
	08 D A 36447 19136 2934 2703 9655 5824 783 623	3.8 3.3 3.7 4.3
	09 D A 36447 18731 3152 2903 9636 8607 808 865	3.8 2.1 3.9 3.4
	17 D A 36447 18731 2971 2262 22203 11926 1793 1545 1.6 1.6 1.7 1.5
	08 D B 36447 19062 2933 2787 7405 3498 568 464	4.9 5.4 5.2 6.0
	09 D B 36478 19243 3110 2650 5495 5153 443 412	6.6 3.7 7.0 6.4
	14 D B 36478 22237 3002 3264 7533 3986 588 589	4.8 5.6 5.1 5.5
	16 D B 36478 19243 3161 2303 15576 7830 1204 1232 2.3 2.5 2.6 1.9
	08 E A 17035 10646 1315 1046 4970 3257 388 287	3.4 3.3 3.4 3.6
	09 E A 17035 10375 1397 1312 4856 4620 392 310	3.5 2.2 3.6 4.2
	14 E A 17035 12759 1327 1346 5081 3983 400 384	3.4 3.2 3.3 3.5
	16 E A 17035 10376 1399 897 10723 6643 832 736	1.6 1.6 1.7 1.2
	08 E B 17035 10529 1318 1177 4735 3033 369 253	3.6 3.5 3.6 4.7
	09 E B 17035 10401 1402 1130 4471 4267 363 320	3.8 2.4 3.9 3.5
	14 E B 17035 12725 1329 1342 4810 3714 377 283	3.5 3.4 3.5 4.7
	16 E B 17035 10402 1396 1033 9987 6202 773 793	1.7 1.7 1.8 1.3

For instance, the composition of P and Q where action a of P synchronizes with either b or c of Q, can be written as ρ(P ) |[b, c]| Q, where ρ maps a onto {b, c}.

For instance, P1 |[a]| (P2 |[]| P3) is equivalent to ρ0((ρ1(P1) |[a1]| ρ2(P2)) |[a2]| ρ3(P3))-observe the different associativity-where ρ1 maps a onto {a1, a2}, ρ2 renames a into a1, ρ3 renames a into a2, and ρ0 renames a1 and a2 into a.

Theorem 2 generalizes easily to more general compositions P || Q (with admissible action mappings) if Q does not contain any action that maps onto a strong action.

Otherwise, our approach coincides with the mono-bisimulation approach of[START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF]. In all the examples addressed in this section, there is always a unique minimal set As, whose identification is made easy using Lemma 1.

Specification available at ftp://ftp.inrialpes.fr/pub/vasy/demos/demo_05

http://rers-challenge.org

Combining Bisimulations Compositionally

The above approach is a mono-bisimulation approach: either the formula is in L dsbr µ and then the system is entirely reduced for divbranching bisimulation, or it is not and then the system is entirely reduced for strong bisimulation. We show in this section that, even if the formula is not in L dsbr µ , it may still be possible to reduce some processes among the parallel processes P 1 , . . . , P n for divbranching instead of strong bisimulation. This approach relies on the fact that, in general, an arbitrary temporal logic formula ϕ may be rewritten in a form that contains both weak modalities, as those present in L dsbr µ , and non-weak modalities of L µ (called strong modalities in this context).

To do so, we characterize a family of fragments of L µ , each of which is written L strong µ (A s ), where A s is the set of actions that can be matched by strong modalities. We then prove that if ϕ belongs to L strong µ (A s ) and some process P i does not contain any action from the set A s , then P i can be reduced for divbranching bisimulation. Throughout this section, we assume that the concurrent system P 1 || . . . || P n is fixed, and we write A for the set of actions occurring in the system. 5 µACTL\X denotes ACTL\X plus fixed points. The authors of [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF] claim that L dsbr µ is as expressive as µACTL\X, but they omit that the ϕ1?.ατ @ weak infinite looping modality cannot be expressed in µACTL\X.

The

Let A s ⊆ A be a fixed set of actions, called strong actions, and let α s denote any action formula such that [[α s ]] A ⊆ A s , called a strong action formula. The fragment L strong µ (A s ) of L µ is defined as the set of formulas that are semantically equivalent to some formula of the following language:

We call α s ϕ 0 a strong modality. L strong µ (A s ) is the fragment of L µ consisting of formulas expressible in a form where strong modalities match only actions in A s . Its formal relationship with L dsbr µ and L µ is given in Theorem 1.

Theorem 1. The following three propositions hold trivially:

Given ϕ ∈ L µ , there exists a (not necessarily unique, see Theorem 3 page 10) minimal set A s such that ϕ ∈ L strong µ (A s ). Obviously, L strong µ (A s ) is not adequate with divbranching bisimulation when A s is not empty, as illustrated by the following example.

Appendix

This appendix is organized as follows. Section A contains the proof of Theorem 2 (page 9). Section B contains the proof of Lemma 1 (page 9). Section C contains the detailed performance data collected from the TFTP experiment presented in Section 4.1.

Note to referees

An archive was created at http://doi.org/10.5281/zenodo.2634149. It contains the experimental material (TFTP and RERS case-studies) and a of this appendix. If the paper is accepted, the URL of the archive will be given in the paper, so that readers can access this companion material and this appendix will be corrected according to the reviewer's comments (if any).

to the previous case. It is important to note that a sequence of infinite τ -transitions (when a i = τ for all i > 0) cannot collapse into an empty sequence, as guaranteed by divbranching bisimulation.

B Proof of Lemma 1 (page 9)

Then the following hold:

Then the following hold:

Proof. It was shown in [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF] that these weak PDL-∆ modalities can be encoded in L dsbr µ when ϕ 0 ∈ L dsbr µ . The proposed encoding also holds when ϕ 0 ∈ L strong µ (A s ). As this encoding does not add more strong modalities than already present in ϕ 0 , then these properties belong to L strong µ (A s ).

Then the following hold:

Proof. It was shown in [START_REF] Mateescu | Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity[END_REF] that the operators of ACTL\X can be encoded using the weak modalities of L dsbr µ . Therefore, the only strong modalities that remain in these formulas are those occurring in ϕ 1 and ϕ 2 , which by definition match only labels in A s . Therefore, these formulas belong to L strong µ (A s ).

In order to prove Lemma 1-4, we need the following lemma:

Proof. This lemma is easily proven by showing that the modal µ-calculus definitions of the left-hand-side and right-hand-side formulas are equivalent. First note that since

A and thus α 2 ϕ = α 2 ∧ ¬τ ϕ for any formula ϕ. We then have the following:

Then the following hold:

Proof. CTL operators are defined on LTS in terms of ACTL\X operators as follows:

In addition, there is the following identity, which is easily proven by showing that the modal µ-calculus definitions of the left-hand-side and right-hand-side formulas are equivalent:

We also use the following standard identity of the modal µ-calculus:

Items 1 to 8 are a direct consequence of Lemma 1-3 and the fact that these operators can be translated to ACTL\X, as shown by equations (Ctl1) to (Ctl8). The proof of Items 9 to 14 follows:

By Lemma 3 and τ / ∈ [[α a ]] A which is in L strong µ (A s ) following Item 6 and Lemmas 1-1 and 1-3.

) is true, then there is a reachable state satisfying ϕ 1 ∧ α a ϕ 2 , by definition of EF. This state also satisfies (ϕ 1 ?.true) * .ϕ 1 ?.α a ϕ 2 , after an empty sequence of steps matching (ϕ 1 ?.true) * . On the other hand, if there is a reachable state satisfying (ϕ 1 ?.true) * .ϕ 1 ?.α a ϕ 2 , then there is a reachable state satisfying both ϕ 1 and α a ϕ 2 , by definition of the weak modality, i.e, the LTS satisfies EF(ϕ 1 ∧ α a ϕ 2 ).

C Detailed performance data of the TFTP case-study

Table 5 presents the detailed performance data obtained on the TFTP casestudy, which served as input to generate the curves of Figure 2 (page 12). Parameters P , S, and I correspond respectively to the property number, the scenario, and the TFTP instance. LTS sizes are given in kilostates, memory in megabytes, and time in seconds. Time does not include LTS generation of the component processes from their LNT specification, which is quite fast (a few seconds) and shared by both the mono-bisimulation approach and the combined bisimulations approach. The column "Ratio Strong/Combined" shows the gain obtained by applying the combined bisimulations approach rather than the mono-bisimulation approach with respect to largest LTS size, memory peak, and time.