Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning

2020·arXiv

Abstract

I. INTRODUCTION

Probabilistic Computation Tree Logic (PCTL) is frequently used to formally specify control objectives such as reachability and safety on probabilistic systems [1]. To check the correctness of PCTL specifications on these systems, model checking methods are required [2]. Although model checking PCTL by model-based analysis is theoretically possible [1], it is not preferable in practice when the system model is unknown or large. In these cases, model checking by sampling, i.e. statistical model checking (SMC), is needed [3], [4].

The statistical model checking of PCTL specifications on Markov Decision Processes (MDPs) is frequently encountered in many decision problems – e.g., for a robot in a grid world under probabilistic disturbance, checking whether there exists a feasible control policy such that the probability of reaching certain goal states is greater than a probability threshold [5]–[7]. In these problems, the main challenge is to search for such a feasible policy for the PCTL specification of interest.

To search for feasible policies for temporal logics speci-fications, such as PCTL, on MDPs, one approach is model-based reinforcement learning [8]–[11] – i.e., first inferring the transition probabilities of the MDP by sampling over each state-action pair, and then searching for the feasible policy via model-based analysis. This approach is often inefficient, since not all transition probabilities are relevant to the PCTL

Nima Roohi is with the University of California San Diego, USA nroohi@ucsd.edu. Matthew West, Mahesh Viswanathan, and Geir E. Dullerud are with the University of Illinois at Urbana-Champaign, USA

specification of interest. Here instead, we adopt a model-free reinforcement learning approach [12].

Common model-free reinforcement learning techniques cannot directly handle temporal logic specifications. One solution is to find a surrogate reward function such that the policy learned for this surrogate reward function is the one needed for checking the temporal logic specification of interest. For certain temporal logics interpreted under special semantics (usually involving a metric), the surrogate reward can be found based on that semantics [13]–[15].

For temporal logics under the standard semantics [16], the surrogate reward functions can be derived via constructing the product MDP [7], [17], [18] of the initial MDP and the automaton realizing the temporal logic specification. However, the complexity of constructing the automaton from a general linear temporal logic (LTL) specification is double exponential [16], [19]. For a fraction of LTL, namely LTL/GU, the complexity is exponential [20], [21]. In addition, the size of the product MDP is usually much larger than the initial MDP, although the produce MDP may be constructed on-the-fly to reduce the extra computation cost, as it did in [18].

In this work, we propose a new statistical model checking method for PCTL specifications on MDPs. For a lucid discussion, we only consider non-nested PCTL specifications. PCTL formulas in general form with nested probabilistic operators can be handled in the standard manner using the approach proposed in [22], [23]. Our method uses upper-confidence-bound (UCB) based Q-learning to directly learn the feasible policy of PCTL specifications, without constructing the product MDP. The effectiveness of UCB-based Qlearning has been proven for the K-bandit problem, and has been numerically demonstrated on many decision-learning problems on MDPs (see [24]).

For bounded-time PCTL specifications, we treat the statistical model checking problem as a finite sequence of K-bandit problems and use the UCB-based Q-learning to learn the desirable decision at each time step. For unbounded-time PCTL specifications, we look for a truncation time to reduce it to a bounded-time problem by checking the PCTL specification and its negation at the same time. Our statistical model checking algorithm is online; it terminates with probability 1, and only when the statistical error of the learning result is smaller than a user-specified value.

The rest of the paper is organized as follows. The preliminaries on labeled MDPs and PCTL are given in Section II. In Section III, using the principle of optimism in the face of uncertainty, we design Q-learning algorithms to solve finite-time and infinite-time probabilistic satisfaction, and give finite sample probabilistic guarantees for the correctness of the algorithms. We implement and evaluate the proposed algorithms on several case studies in Section IV. Finally, we conclude this work in Section V.

II. PRELIMINARIES AND PROBLEM FORMULATION

The set of integers and real numbers are denoted by N and R, respectively. For , let [n] = {1, . . ., n}. The cardinality of a set is denoted by . The set of finite-length sequences taken from a finite set S is denoted by .

A. Markov Decision Process

A Markov decision process (MDP) is a finite-state probabilistic system, where the transition probabilities between the states are determined by the control action taken from a given finite set. Each state of the MDP is labeled by a set of atomic propositions indicating the properties holding on it, e.g., whether the state is a safe/goal state.

Definition 1: A labeled Markov decision process (MDP) is a tuple M = (S, A, T, AP, L) where

• S is a finite set of states.

• A is a finite set of actions. • is a partial transition probability function. For any state and any action ,

With a slight abuse of notation, let A(s) be the set of allowed actions on the state s.

• AP is a finite set of labels.

• is a labeling function.

Definition 2: A policy decides the action to take from the sequence of states visited so far. Given a policy and an initial state , the MDP M becomes purely probabilistic, denoted by . The system is not necessarily Markovian.

B. Probabilistic Computation Tree Logic

The probabilistic computation tree logic (PCTL) is defined inductively from atomic propositions, temporal operators and probability operators. It reasons about the probabilities of time-dependent properties.

Definition 3 (Syntax): Let AP be a set of atomic propositions. A PCTL state formula is defined by

where is a (possibly infinite) time horizon, and is a threshold.1 The operators and are called probability operators, and the “next”, “until” and “release” operators are called temporal operators.

More temporal operators can be derived by composition: for example, “or” is ; “true” is ; “finally” is ; and “always” is . For simplicity, we write and as U, R, F and G, respectively.

Definition 4 (Semantics): For an MDP M = (S, A, T, , the satisfaction relation |= is defined by for a state s or path by

where . And means the path is drawn from the MDP M under the policy , starting from the state s from.

The PCTL formulas (or ) mean that the maximal (or minimal) satisfaction probability of “next” is . The PCTL formulas (or ) mean that the maximal (or mini- mal) satisfaction probability that holds “until” holds is .

III. NON-NESTED PCTL SPECIFICATIONS

In this section, we consider the statistical model check- ing of non-nested PCTL specifications using an upper-confidence-bound based Q-learning. For simplicity, we focus on and where and are atomic propositions. Other cases can be handled in the same way. We discuss the case of T = 1 in Section III-A, the case of T > 1 in Section III-B, and the case of in Section III-C. Similar to other works on statistical model checking [3], [4], we make the following assumption.

Assumption 1: For and with and , we assume that and , respectively.

When it holds, as the number of samples increases, the samples will be increasingly concentrated on one side of the threshold p by the Central Limit Theorem. Therefore, a statistical analysis based on the majority of the samples has increasing accuracy. When it is violated, the samples would be evenly distributed between the two sides of the boundary p, regardless of the sample size. Thus, no matter how the sample size increases, the accuracy of any statistical test would not increase. Compared to statistical model checking algorithms based on sequential probability ratio tests (SPRT) [25], [26], no assumption on the indifference region is required here. Finally, by Assumption 1, we have the additional semantic equivalence between the PCTL speci-fications: and ; thus, we will not distinguish between them below.

For further discussion, we first identify a few trivial cases. For , let

Then for any policy if ; and if . The same holds for by defining to be the union of end components of the MDP M labeled by (this only requires knowing the topology of M) [16]. In the rest of this section, we focus on handling the nontrivial case .

A. Single Time Horizon

When T = 1, for any , the PCTL specification (or ) holds on a random path starting from the state s if and only if , where and are from (1). Thus, it suffices to learn from samples whether

where

and means is drawn from the transition probability for state s and action a. This is an |A(s)|-arm bandit problem; we solve this problem by upper-confidence-bound strategies [27], [28].

Specifically, for the iteration k, let be the number samples for the one-step path , and with a slight abuse of notation, let

The unknown transition probability function is estimated by the empirical transition probability function

And the estimation of from the existing k samples is

Since the value of the Q-function is bounded, we can construct a confidence interval for the estimate with statistical error at most using Hoeffding’s inequality by

where we set the value of the division to be for .

Remark 1: We use Hoeffding’s bounds to yield hard guarantees on the statistical error of the model checking algorithms. Tighter bounds like Bernstein’s bounds [29] can also be used, but they only yield asymptotic guarantees on the statistical error.

The sample efficiency for learning for the bandit problem (2) depends on the choice of sampling policy, decided from the existing samples. A provably best solution is to use the Q-learning from [27], [28]. Specifically, an upper confidence bound (UCB) is constructed for each state-action pair using the number of samples and the observed reward, and the best action is chosen with the highest possible reward, namely the UCB. The sampling policy is chosen by maximizing the possible reward greedily:

The action is chosen arbitrarily when there are multiple candidates. The choice of in (7) ensures that the policy giving the upper bound of the value function gets most frequently sampled in the long run.

To initialize the iteration, the Q-function is set to

to ensure that every state-action is sampled at least once. The

where p is the probability threshold in the non-nested PCTL formula. Remark 2: For or , it suffices to change the termination condition (9) by returning true if , and returning false if . The same statements hold for general PCTL specifications, as discussed in Sections III-B and III-C Now, we summarize the above discussion by Algorithm 1 and Theorem 1 below. Theorem 1: The return value of Algorithm 1 is correct with probability at least . Proof: We provide the proof of a more general state- ment in Theorem 2.

Require: MDP M, parameter .

4: Sample from M, and update the transition probability function by (3)(4).

5: Update the bounds on the Q-function and the policies by (6)(7).

Remark 3: The Hoeffding bounds in (6) are conservative. Consequently, as shown in the simulations in Section IV, the actual statistical error of the our algorithms can be smaller than the given value. However, as the MDP is unknown, finding tighter bounds is challenging. One possible solution is to use asymptotic bounds, such as Bernstein’s bounds [29]. Accordingly, the algorithm will only give asymptotic probabilistic guarantees.

B. Finite Time Horizon

When , for any , let

i.e., and are the maximal satisfaction probability of for a random path starting from s for any policy and any policy with first action being a, respectively. By definition, and satisfy the Bellman equation

The second equality of the second equation is derived from

by the semantics of PCTL.

From (11), we check by induction on the time horizon T . For , the lower and upper bounds for can be derived using the bounds on the value function for the previous step — for h = 1 from (6) and for

h > 0 by the following lemma.

and

where is a parameter such that with probability at least . The bounds in (12) are derived from (11) by applying Hoeffding’s inequality, using the fact that and the Q-functions are bounded within [0, 1].

From the boundedness of , we note that this confidence interval encompasses the statistical error in both the estimated transition probability function and the boundsand of the value function. Accordingly, the policy chosen by the OFU principle at the h step is

with an optimal action chosen arbitrarily when there are multiple candidates, to ensure that the policy giving the upper bound of the value function is sampled the most in the long run. To initialize the iteration, the Q-function is set to

for all , to ensure that every state-action is sampled at least once.

Sampling by the updated policy can be performed in either episodic or non-episodic ways [24]. The only requirement is that the state-action pair should be performed frequently for each and for each state s satisfying . In addition, batch samples may be drawn, namely sampling over the state-action pairs multiple times before updating the policy. In this work, for simplicity, we use a non-episodic, non-batch sampling method, by drawing

for all and state s such that . The Q-function and the value function are set and initialized

Require: MDP M, parameters for .

1: Initialize the Q-function and the policy by (15)(14). 2: Obtain and by (1).

4: Sample by (16), and update the transition probability function by (3)(4).

5: Update the bounds by (12)(13) and the policy by (14).

by (13) and (15). The termination condition is give by

where p is the probability threshold in the non-nested PCTL formula. The above discussion is summarized by Algorithm 2 and Theorem 2. Theorem 2: Algorithm 2 terminates with probability 1 and its return value is correct with probability at least , where . Proof: By construction, as the number of iterations . Thus, by Assumption 1, the termination condition (17) will be satisfied with probability 1. Now, let E be the event that the return value of Algorithm 2 is correct, and let be the event that Algorithm 2 terminates at the iteration k, then we have . For any k, the event E happens given that holds, if the Hoeffding confidence intervals given by (12) hold for any actions , and state s with . Thus, we have , where N = , implying that the return value of Algorithm 2 is correct with probability . By Theorem 2, the desired overall statistical error splits into the statistical errors for each state-action pair through the time horizon. For implementation, we can split it equally by . The specification can be handled by replacing argmax with argmin in (14), and max with min in (13). The termination condition is the same as (17). Remark 4: Due to the semantics in Definition 4, running Algorithm 2 proving or disproving is easier than disproving or proving ; and the difference increases with the number of actions |A| and the time horizon T . This is because proving or disproving requires only finding and evaluating some policy with , while disproving it requires evaluating all possible policies with sufficient accuracy. This is illustrated by the simulation results presented in Section IV.

C. Infinite Time Horizon

Infinite-step satisfaction probability can be estimated from finite-step satisfaction probabilities, using the monotone convergence of the value function in the time step H,

where p is the probability threshold in the non-nested PCTL formula.

The general idea in using the monotonicity to check infinite horizon satisfaction probability in finite time is that if we check both and its negation at the same time, one of them should terminate in finite time. Here and are treated as atomic propositions. We can use Algorithm 2 to check their satisfaction probabilities for any time horizon T simultaneously. The termination in finite time is guaranteed, if the time horizon for both computations increase with the iterations. The simplest choice is to increase H by 1 for every K iterations; however, this brings the problem of tuning K. Here, we use the convergence of the best policy as the criterion for increasing H for each satisfaction computation. Specifically, for all the steps h in each iteration, in addition to finding the optimal policy with respect to the upper confidence bounds of the Q-functionsby (14), we also consider the the optimal policy with respect to the lower confidence bounds of the Q-functions . Obviously, when argmax, we know that the policy is optimal for all possible Q-functions within . This implies that these bounds are fine enough for estimating ; thus, if the algorithm does not terminate by the condition (19), we let

stops and the largest time horizon is H, then the return value is correct with probability at least . Thus, the theorem holds.

Remark 5: By Theorem 3, given the desired overall con-fidence level , we can split it geometrically by , where .

Remark 6: Similar to Section III-B, checking for is derived by replacing argmax with argmin in (14), and max with min in (13). The termination condition is the same as (19).

Remark 7: Finally, we note that the exact savings of sample costs for Algorithms 2 and 3 depend on the structure of the MDP. Specifically, the proposed method is more efficient than [9], [10], [30], when the satisfaction probabilities differ significantly among actions, as it can quickly detect suboptimal actions without over-sampling on them. On the other hand, if all the state-action pairs yield the same Q-value, then an equal number of samples will be spent on each of them — in this case, the sample cost of Algorithms 2 and 3 is the same as [9], [10], [30].

IV. SIMULATION

To evaluate the performance of the proposed algorithms, we ran them on two different sets of examples. In all the simulations, the transition probabilities are unknown to the algorithm (this is different from [9]).

The first set contains 10 randomly generated MDPs with different sizes. For these MDPs, we considered the formula for the finite horizon, and for the infinite horizon. In both cases, , and H are chosen arbitrarily. The second set contains 9 versions of the Sum of Two Dice program. The standard version [31] models the sum of two fair dice, each with 6 different possibilities numbered 1, . . . , 6. To consider MDPs with different sizes, we consider 9 cases where each dice is still fair, but has n possibilities numbered 1, . . . , n, with n = 3 in the smallest example, and n = 17 in the largest example. For these MDPs, we considered the formula for the finite horizon, and for the infinite horizon. In both cases encodes the atomic predicate that is true iff values of both dice are chosen and their sum is less than an arbitrarily

CHECKING PROPOSITIONS ARE CHOSEN ARBITRARILY. COLUMN

chosen constant. Also, in the finite case, H = 5 in the smallest example and 10 everywhere else.

For each MDP, we first numerically estimate the values of and , for the randomly generated MDPs, and , and , for the variants of the two-dice examples, using the known models on PRISM [32]. Then, we use Algorithms 2 and 3 on the example models with only knowledge of the topology of the MDPs and without knowing the exact transition probabilities. For every MDP, we tested each algorithm with two different thresholds p, one smaller and the other larger than the estimated probability, to test the proposed algorithms, with set to 5%. We ran each randomly generated test 100 times and each two-dice variant test 10 times. Here we only report average running time and average number of iterations. All tests returned the correct answers — this suggests that the Hoeffding’s bounds used in the proposed algorithms are conservative (see Remark 3). The algorithms are implemented in Scala and ran on Ubuntu 18.04 with i7-8700 CPU 3.2GHz and 16GB memory.

Tables I and II show the results for finite horizon reachability. An interesting observation in these tables is that in all examples, disproving the formula is 3 to 100 times faster. We believe this is mainly because, to disprove , all we need is one policy for which holds. However, to prove , one needs to show that every policy satisfies (see Remark 4).

Tables III and IV show the results for infinite horizon reachability. Note that Algorithm 3 considers both the formula and its negation, and contrary to the finite horizon reachability, disproving a formula is not always faster for the infinite case. In most of the larger examples that are randomly generated, and are very small on average. This shows that in these examples, the algorithm was smart enough to learn there is no need to increase H in order to

CHECKING ON VARIANTS OF SUM-OF-TWO-DICE MDPS. ATOMIC PROPOSITION IS TRUE IFF BOTH DICE HAVE CHOSEN THEIR

COLUMN IS THE NUMBER OF ALTERNATIVES ON EACH DICE. EACH MDP HAS TWO ACTIONS (i.e.

CHECKING ARE VALUES OF THE CORRESPONDING VARIABLES IN ALGORITHM 3 AT

solve the problem. However, this is not the case for two-dice examples. We believe this is because in the current implementation, the decision to increase H does not consider the underlying graph of the MDP. For example, during the execution, if the policy forces the state to enter a self-loop with only one enabled action, which is the case in two-dice examples, then after every iteration the value of H will be increased by 1.

V. CONCLUSION

We proposed a statistical model checking method for Probabilistic Computation Tree Logic on Markov decision processes using reinforcement learning. We first checked PCTL formulas with bounded time horizon, using upper-

CHECKING AND ARE VALUES OF THE CORRESPONDING VARIABLES IN ALGORITHM 3 AT TERMINATION.

confidence-bounds based Q-learning, and then extended the technique to unbounded-time specifications by finding a proper truncation time by checking the specification of interest and its negation at the same time. Finally, we demonstrated the efficiency of our method on several case studies.

REFERENCES

[1] C. Baier, B. Haverkort, H. Hermanns, and J. Katoen, “Model-checking algorithms for continuous-time Markov chains,” IEEE Transactions on Software Engineering, vol. 29, no. 6, pp. 524–541, 2003.

[2] Handbook of Model Checking, 2018.

[3] K. G. Larsen and A. Legay, “Statistical Model Checking: Past, Present, and Future,” in Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, 2016, pp. 3–15.

[4] G. Agha and K. Palmskog, “A Survey of Statistical Model Checking,” ACM Trans. Model. Comput. Simul., vol. 28, no. 1, pp. 6:1–6:39, 2018.

[5] G. E. Fainekos, A. Girard, H. Kress-Gazit, and G. J. Pappas, “Temporal logic motion planning for dynamic robots,” Automatica, vol. 45, no. 2, pp. 343–352, 2009.

[6] H. Kress-Gazit, M. Lahijanian, and V. Raman, “Synthesis for Robots: Guarantees and Feedback for Robot Behavior,” Annual Review of Control, Robotics, and Autonomous Systems, vol. 1, no. 1, pp. 211– 236, 2018.

[7] A. K. Bozkurt, Y. Wang, M. Zavlanos, and M. Pajic, “Control synthesis from linear temporal logic specifications using model-free reinforcement learning,” in IEEE International Conference on Robotics and Automation (ICRA) (Submitted), 2020.

[8] D. Henriques, J. G. Martins, P. Zuliani, A. Platzer, and E. M. Clarke, “Statistical Model Checking for Markov Decision Processes,” in 2012 Ninth International Conference on Quantitative Evaluation of Systems, 2012, pp. 84–93.

[9] T. Br´azdil, K. Chatterjee, M. Chmel´ık, V. Forejt, J. Kˇret´ınsk´y, M. Kwiatkowska, D. Parker, and M. Ujma, “Verification of Markov Decision Processes Using Learning Algorithms,” in Automated Technology for Verification and Analysis, 2014, pp. 98–114.

[10] J. Fu and U. Topcu, “Probably Approximately Correct MDP Learning and Control With Temporal Logic Constraints,” arXiv:1404.7073 [cs], 2014.

[11] P. Ashok, J. Kˇret´ınsk´y, and M. Weininger, “PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games,” arXiv:1905.04403 [cs], 2019.

[12] R. S. Sutton and A. G. Barto, “Reinforcement Learning: An Introduction,” p. 352, 2018.

[13] X. Li, C.-I. Vasile, and C. Belta, “Reinforcement Learning With Temporal Logic Rewards,” arXiv:1612.03471 [cs], 2016.

[14] A. Jones, D. Aksaray, Z. Kong, M. Schwager, and C. Belta, “Robust Satisfaction of Temporal Logic Specifications via Reinforcement Learning,” arXiv:1510.06460 [cs], 2015.

[15] M. L. Littman, U. Topcu, J. Fu, C. Isbell, M. Wen, and J. MacGlashan, “Environment-Independent Task Specifications via GLTL,” arXiv:1704.04341 [cs], 2017.

[16] C. Baier and J.-P. Katoen, Principles of Model Checking, 2008.

[17] E. M. Hahn, M. Perez, S. Schewe, F. Somenzi, A. Trivedi, and D. Wojtczak, “Omega-Regular Objectives in Model-Free Reinforcement Learning,” in Tools and Algorithms for the Construction and Analysis of Systems, 2019, vol. 11427, pp. 395–412.

[18] M. Hasanbeig, Y. Kantaros, A. Abate, D. Kroening, G. J. Pappas, and I. Lee, “Reinforcement learning for temporal logic control synthesis with probabilistic satisfaction guarantees,” in Proceedings of the 58th Conference on Decision and Control. IEEE, 2019, pp. 5338–5343.

[19] E. M. Hahn, G. Li, S. Schewe, A. Turrini, and L. Zhang, “Lazy Probabilistic Model Checking without Determinisation,” arXiv:1311.2928 [cs], 2013.

[20] D. Kini and M. Viswanathan, “Complexity of model checking mdps against LTL specifications,” in 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017, December 11-15, 2017, Kanpur, India, ser. LIPIcs, S. V. Lokam and R. Ramanujam, Eds., vol. 93. Schloss Dagstuhl - Leibniz-Zentrum f¨ur Informatik, 2017, pp. 35:1–35:13.

[21] ——, “Limit deterministic and probabilistic automata for ltlInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2015, pp. 628–642.

[22] K. Sen, M. Viswanathan, and G. Agha, “Statistical Model Checking of Black-Box Probabilistic Systems,” in Computer Aided Verification, 2004, pp. 202–215.

[23] ——, “On Statistical Model Checking of Stochastic Systems,” in Computer Aided Verification, 2005, vol. 3576, pp. 266–280.

[24] C. Szepesv´ari, “Algorithms for Reinforcement Learning,” Synthesis Lectures on Artificial Intelligence and Machine Learning, vol. 4, no. 1, pp. 1–103, 2010.

[25] P. Zuliani, “Statistical model checking for biological applications,” International Journal on Software Tools for Technology Transfer, vol. 17, no. 4, pp. 527–536, 2015.

[26] Y. Wang, N. Roohi, M. West, M. Viswanathan, and G. E. Dullerud, “Statistical verification of PCTL using stratified samples,” in 6th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS), IFACPapersOnLine, vol. 51, 2018, pp. 85–90.

[27] V. Kuleshov and D. Precup, “Algorithms for multi-armed bandit problems,” arXiv:1402.6028 [cs], 2014.

[28] S. Bubeck, “Regret Analysis of Stochastic and Nonstochastic Multiarmed Bandit Problems,” Foundations and Trends Rin Machine Learning, vol. 5, no. 1, pp. 1–122, 2012.

[29] V. Mnih, C. Szepesv´ari, and J.-Y. Audibert, “Empirical Bernstein stopping,” in Proceedings of the 25th International Conference on Machine Learning - ICML ’08, 2008, pp. 672–679.

[30] B. Balle and M. Mohri, “Learning Weighted Automata,” in Algebraic Informatics, 2015, vol. 9270, pp. 1–21.

[31] D. Knuth and A. Yao, Algorithms and Complexity: New Directions and Recent Results. Academic Press, 1976, ch. The complexity of nonuniform random number generation.

[32] M. Kwiatkowska, G. Norman, and D. Parker, “PRISM 4.0: Verification of Probabilistic Real-Time Systems,” in Computer Aided Verification, 2011, vol. 6806, pp. 585–591.

Designed for Accessibility and to further Open Science