Colin Armstrong

Helen Armstrong

7 MODELING FORENSIC EVIDENCE SYSTEMS USING DESIGN SCIENCE

Keywords: Design science research, socio-technology, forensic evidence

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

INTRODUCTION

Design science is not just a methodology for devising solutions utilizing technology. It is an approach that offers the researcher the ability to investigate problem spaces and devise theories and designs that could address such problem spaces. Most problem spaces encompass various stakeholders, each with a particular perspective on that problem. The field of forensic evidence is no different, with three main stakeholder groups: law enforcement, the first responders to a crime situation; forensic scientists, who take physical items (DNA, weapons, disk drives, mobile phone, etc.) and, using scientific standards and methodologies, form opinions and interpretations of the evidence; and the judiciary, who employ information about the evidence derived from law enforcement and forensic science to present arguments for either the prosecution or defense.

Electronic devices are increasingly appearing as important items of evidence in criminal investigations, due to the spread of technology and society's dependence upon that technology in everyday life. Although digital forensics is a frequent topic in information systems security research, the focus in this area is broadening to consider the links between all types of forensic evidence (digital and otherwise) for many types of traditional crime, not just computer crime. This is due to the increasing amount of potential evidence stored electronically on devices such as computers, Internet and ISP servers, mobile phones, portable storage devices, and other electronic devices and media for traditional and digital crimes.

Investigation of the area of evidence illustrates a number of problems emerging as technology becomes more pervasive. Using design science as the chosen research approach, this paper describes a study of the forensic evidence problem space through the perspectives of the three main stakeholder groups and the design of a meta-model for the effective management of forensic evidence at the tactical level. The meta-model presented provides an opportunity to employ a number of different technological solutions, depending upon the perspective and needs of the interested party. As law enforcers are the stakeholders with the majority of exposure to, and interaction with, evidence, the evaluation of the suggested processes and models has been undertaken by a focus group of experienced law enforcement officers.

WHY DESIGN SCIENCE?

Evidence takes the form of both physical objects and information about those objects. Evidence can be comprised of fragments of disparate data that combine to produce something larger and more meaningful in the context of the investigation. So why design science? In design science research, "knowledge and understanding of a problem domain and its solution are achieved in the building and application of the designed artifact" (Hevner et al. 2004, p. 75). Furthermore, design science attempts to create things that serve human needs [START_REF] March | Design Science and Natural Science Research on Information Technology[END_REF] and benefits those affected by the problem situation. With the focus on designing solutions Design Science is an ideal approach for the analysis of the forensic evidence problem space and the design of a model to eliminate or reduce that problem domain.

DESIGN SCIENCE AND SOFT APPROACHES

Much of the literature in support of design science focuses on the engineering or "hard" side involving scientific rigor pertaining to the physical artifact and technology (together with the associated systems development). However, the "soft" side of information systems recognizing the social and organizational aspects is also emerging. [START_REF] Baskerville | Soft Design Science Research: Extending the Boundaries of Evaluation in Design Science Research[END_REF] highlight the need for a soft design science research approach to accommodate IT/IS artifacts in natural organizational settings. Information systems encompass both social, human, and organizational aspects, as well as tools and technology, and all of these aspects need to be considered in problem studies and the associated solution design. [START_REF] Checkland | Soft Systems Methodology in Action[END_REF] discuss the need to recognize that problems are seen through the world view of an individual, which they refer to as the weltanschauung. Human beings "interpret what they perceive. Moreover, the interpretation may, in principle, be unique to a particular observer. This means that multiple perspectives are always available" (Checkland and Scholes 1990, p. 25). In the context of this research the authors propose that world views can be either individual or group perspectives, depending upon the nature and scope of the problem domain under consideration. A full understanding of the problem situation incorporating the perspectives of the different stakeholders provides a holistic view for those attempting to design solutions. Softer approaches also permit the consideration of social and political issues that form an integral part of problem situations. The consideration of human and organizational issues is crucial for the design and implementation of effective solutions. [START_REF] March | Design Science and Natural Science Research on Information Technology[END_REF] and [START_REF] March | Design Science in the Information Systems Discipline: An Introduction to the Special Issue on Design Science Research[END_REF] propose the two cornerstones of design science as building and evaluating artifacts. In order to design, build, and evaluate artifacts, it is necessary to understand the problem causes and impact to ensure that the artifact does actually address the problem.

THE PROBLEM SPACE

A problem exists when a stakeholder in a given situation perceives there is a difference between the desired state and the current state [START_REF] Checkland | Soft Systems Methodology in Action[END_REF][START_REF] Jayaratna | Understanding and Evaluating Methodologies[END_REF][START_REF] Jonassen | Toward a Design Theory of Problem Solving[END_REF]. Key to the recognition of a problem is that a stakeholder group affected by the situation perceives a gap between the two states. The same problem can be perceived differently by each stakeholder group within the problem situation based upon their perspective of the world. In order to fully understand a problem situation, the perspectives of different stakeholder groups must be considered. To be of value and significance, design science should address a class of problem (faced by a collection rather than by one individual), be nontrivial in nature (significant), as well as relevant (germane and useful).

A clear understanding of the problem and its causes is needed in order to develop a theory relating to the design of a solution and also before an in-depth design of a solution is embarked upon. As the aim is to reduce or eliminate the problem space, interaction with theory conceptualization and development, the solution design process, plus the solution evaluation is essential.

THE SOLUTION SPACE

Inextricably linking the problem and solution spaces is the theory space. [START_REF] Walls | Building an Information Systems Design Theory for Vigilant EIS[END_REF] differentiated design theory from scientific theory by considering the overall objectives of each. While scientific theory seeks to understand and predict natural phenomenon, the aim of design theory is to guide artifact creation. [START_REF] March | Design Science and Natural Science Research on Information Technology[END_REF] and later also [START_REF] Venable | The Role of Theory and Theorising in Design Science Research[END_REF] note the interchangeable nature of models and theories as forms for representing knowledge Venable highlights the importance and inclusion of theory building as a specific component of the design science research process, claiming that theorizing and theory building actually occur before, during, throughout, at the end, and as a result of design science research. Venable proposes a cyclic approach that recognizes the central role played by theory and theorizing.

The theory realm holds value as the theory or hypothesis is expressed in a design with particular application to the given problem space. The theory realm also is dependent on the stakeholder's perspective. Where particular stakeholder groups are removed from consideration, there will be no debate or understanding of the holistic situation. A holistic viewpoint facilitates and promotes a successful solution design and ownership of the artifact.

The design is a conceptualization of a specified solution that is one of many potential solutions envisaged to reduce or eliminate the problem. Each potential solution is an instantiation of a conceptualization and, in information systems terms, a solution design could be a detailed physical model illustrating application in a specific in situ or a logical model that could be applied in a number of physical modes.

A project to investigate the problem space in forensic evidence management and the design of a socio-technological solution space has been undertaken. With a strong sociopolitical element, the solution design devised took the form of a meta-model enveloping, a number of lower-level interactive models to shape a management system. An iterative approach was employed in this research using three main stages of data collection and analyses (see Figure 1). The stakeholders were interviewed in three groups over a period of two years, with participants in the judiciary, forensic practitioners, and law enforcement stakeholder groups interviewed in each period. This enabled a gradual development of the model together with solutions on a progressive basis. The data gathered in stages 2 and 3 was used to confirm the findings from the interviews in earlier stages and further develop the new model and solutions.

FORENSIC EVIDENCE PROBLEM SPACE

The essence of the forensic evidence problem space is the disparate conceptualization of the usage and tactical management of evidence. Exposure and association with forensic evidence by the three primary perspective groups is sequential in nature and the three groups do not enjoy forensic evidence associations equally. A simplistic observation would describe law enforcement as the first responders, forensic scientists as the experts, and the judiciary as that highly respected independent determinator of an accused's fate. The problem space of the forensic evidence management project is illustrated in the rich picture presented in Figure 2. The nature, purpose, and importance of forensic evidence is viewed differently by each of the stakeholder groups and, with no common understanding or standards to underpin the realm, misunderstandings commonly arise. Once a perceived wrong has been brought to the attention of the enforcers of law, an enquiry may commence and, to discover the facts behind the perceived wrong, evidence is sought. To better interpret and understand the meaning of evidence, we rely on scientific expertise. Finally, when sufficient information is gathered, it is presented in order to persuade the finder of fact in determining an accused's guilt. The association between evidence and each of these three perspectives reflects very different relationships, as can be seen in Figure 2.

The law enforcement community has the greatest exposure to forensic evidence. It identifies and collects the evidence at the scene of a violation; it manages the safe handling of the evidence in order for it to be admissible to a court of law; it directs the appointment of forensic scientists for evidence analysis and collates forensic results; and finally, it presents evidence in court predominantly representing the prosecution. Forensic scientists carry out testing and analyses specific to the inquiry, and the judiciary presents evidence to support an argument of guilt or non-guilt.

The lack of standard procedures, underlying classifications, and international standards relating to evidence, as well as differing laws, has a major effect upon law enforcers, in comparison to the minor influence it plays for the judiciary and forensic scientists.

Law Enforcement

Law enforcers are held responsible, not only as first responders to secure evidence locations; in most situations, they are solely responsible for the collection and management of forensic evidence. Law enforcers are considered less-educated blue collar workers and, therefore, not as well qualified to assess issues as forensic scientists or the judiciary. They tend to be faced with the chaotic frontier of humanity at its worst and tasked with responsibility for forensic evidence management while being required to preserve peace and security in our communities. This situation results in little or no time for law enforcers to contemplate the intricacies of an incident and, because anything could be evidence, adopt the practice of collecting everything.

Law enforcers do not have internationally agreed standards ensuring unified best practices for forensic evidence processes, relying on jurisdictional policies and procedures. This does not suggest that law enforcers do a poor job. It does suggest, however, that even though there is a great deal of international cooperation and that enforcement agencies and personnel strive to provide the best service, there is little national or global agreement as to what constitutes best practice and service.

Forensic Scientists

Unless working alongside law enforcers, forensic scientists are not first responders, do not secure evidence locations, do not collect evidence, and are only responsible for the management of forensic evidence while it is in their care for analysis. Forensic scientists often become involved only after law enforcers have collected potential evidence. As forensic scientists usually have university education in a scientific field, they are perceived to be educated and professional experts in their particular domain of research. This group is perceived to be experts without a bias toward either prosecution or defense because they pursue discovery of facts based on dispassionate scientific methods. Hence, forensic scientists are perceived to be divorced from determinations of guilt or otherwise.

Forensic experts are regularly afforded the luxury of retiring to a secured laboratory far from the influences of a chaotic world and, therefore, have more time and an environment more conducive to contemplating the meaning of evidence items. Forensic experts are often excluded from the rest of an enquiry and only called upon for specialized expert opinion. When granted access to complete case file information, forensic experts do have time to contemplate the intricacies of an incident. Generally, forensic scientists are only associated with particular items of case evidence and not with every collected item.

As scientists, forensic scientists are members of organizations that are international and that establish and maintain agreed standard practices for conducting scientific processes. Many fields within forensic science have their own classification systems or methods of categorizing objects; however, these are isolates and form well-defined boundaries resulting is discrete, unintegrated systems.

Judiciary

Although the judiciary group members fall into three separate subgroupsprosecution, defense, and finder of fact-they have yet another point of view relating to evidence. Judiciary group members tend to focus most strongly on interpretations of evidence that support their particular objective: either proving guilt, defending and disputing evidence interpretations, or passing culpability judgement. The judiciary are rarely first responders; they are not responsible for securing evidence locations or collecting evidence, but they are responsible for the management of forensic evidence if it is given into their care.

In contrast to the law enforcement and the forensic science stakeholders, the judiciary believe the evidence itself is not the key factor, but their presentation of the argument pertaining to that evidence in a court of law, or in other words their ability to persuade the finders of fact of guilt or innocence. The judiciary is perceived by society as being highly educated as well as respected, independent determiners of an accused's fate. The judiciary often deals with the worst results from the chaotic frontier of humanity, but does so in the comfort of a secured environment. The judiciary is not perceived as being expert in scientific matters but do have access to specialized publications relating scientific matters to the law and legal precedents. This group specializes in contemplation of evidence, its meanings, and the case in question before the courts and, by ensuring decisions are not hasty, engenders the perception that evidence matters are well and carefully contemplated. However, the judiciary only deals with a small but essential selection of the total collected case evidence and features only that evidence supporting the prosecution or defense case.

The judiciary maintains a deep abidance to rigorously established rules and procedures relating to evidence that are accepted internationally even though the same set of rules are not applied in the same manner in every jurisdiction.

Global and Local Problems

The resulting operational situation presents law enforcers with having to resolve a problem situation because it has greater impact on their operations than the other two perspective groups. The forensic scientists are, for the most part, isolated from the entire case under investigation and limited to providing an expert opinion of the evidence based on scientific principles. Finally, the judiciary determine justice based on only that small amount of evidence essential to argue their case.

The problems emerging from this consideration are both global and local, and include

• a lack of international standards, policies, and procedures for the identification, collection, analysis and presentation of evidence • no classification systems for evidence, only classifications and categorization for certain types of objects that may be used as evidence • the lack of tools and techniques to provide a big picture in the consideration of criminal cases, resulting in a piecemeal rather than informed, holistic approach to decision making about evidence • the bias of perspective and the different perspectives of the stakeholders, resulting in the value of evidence being viewed differently by each of the stakeholder groups

FORENSIC EVIDENCE THEORY AND MODEL DESIGN

An extensive archival search was conducted to identify prior work done to address the above problems and any standards or models already developed in the area. The findings were that the work has been piecemeal with no interdisciplinary solutions proposed. In all, 52 professionals across the three domains were interviewed and data collected regarding the nature of evidence, the problems they faced, and a desired state. A set of models was then developed based on analyses of that data.

The models, designed to reflect perspectives in forensic evidence tactical management, draw upon established theories and modeling approaches. The journey along the evidence path from raw data to courtroom-presented evidence is at times complex and chaotic. No single theory adequately addresses the modeling of forensic evidence. There are two main streams of theory providing the elements underpinning such modeling. The first approach addresses the organization of evidence, which draws on theories associated with systems. The second approach accommodates the nature of evidence, which includes legal perspectives.

General systems theory is the overriding approach to the organization of evidence and associated information. To this are incorporated elements from a number of interconnected theoretical bases including chaos theory, complexity theory, network theory, social-network theory, and actor-network theory.

The overriding theories addressing the legal perspective are legal theory and evidence theory, which are strongly linked with justice and policing theories. As burdens of proof are not absolute they are dealt with as probability values. Probability theory is in turn accompanied by Bayesian statistical theory and Dempster-Shafer theory. In addition to theories, principles such as Locard's exchange principle are applied to the analysis of crime scenes.

Other theories contributing to the design of these models include elements from Heisenberg's uncertainty principle, information theory, scientific theory, model theory, and stakeholder theory. The development of the designed models draws on elements from these theory foundations.

The aim was to design a high-level conceptual model that provided an interdisciplinary view of tactical management of forensic evidence. Such an approach offers a broad opportunity to satisfactorily address the challenges presented in the forensic evidence problem space. A unifying holistic forensic evidence model necessarily consists of components specifically designed to address both global and local problems. There are six components considered desirable for inclusion in a model for the tactical management of forensic evidence processing.

1. A method for understanding the transitional information flow as raw data related to forensic evidence changes to become evidence due to the information that practitioners extract from the raw collected data and convert into knowledge. 2. A method for determining the particular relationship between the enquirer and the evidence. 3. A system for examining the interrelatedness of forensic evidence in a network of case evidence. 4. A method of visualizing forensic evidence networks. 5. A repository for forensic evidence information. 6. A system to accommodate classification of forensic evidence, and provide standards and best practices.

The Armstrong forensic evidence meta-model (see Figure 3) brings together the six components identified as desirable for the tactical management of forensic evidence processing. Modeling the six components reveals that four components are processes and two are frameworks. Modeling also reveals that two components address sociological aspects and four components address technological aspects of forensic evidence. The six models forming the meta-model are • evidence data to knowledge conversion • evidence stakeholder perspective • evidence relationships network • evidence resource library • evidence network analysis • evidence classification scheme

The evidence data to knowledge conversion process (see Figure 4) models an entry point into the inquiry-related data and provides the mechanism for determining the status of evidence entering an inquiry. Some data is self evident in nature and less disputable than other data. During the processes inculcated in this model, initial statistical data col-Figure 3 The Armstrong Forensic Evidence Meta-Model lection commences and practitioners form conclusions based on the accumulation of data. The major contribution of this process is in the modeling of data integrity entering an inquiry.

During the inquiry process, all incoming evidence arrives, initially, as data, and in a spasmodic manner. Then, as reasoning and analysis commences, the data undergoes a transitional process that sees some data progress to become knowledge based on information processing while other data items may be held awaiting further clarification, discounted, or discarded. Evidence can only exist in the human mind and it is that information that persuades. Forensic evidence is that information that persuades to a level determined by the court within a jurisdiction's legal system. Commonly in matters of civil dispute the burden of proof is "in all likelihood," and in criminal matters the burden of proof is "beyond a reasonable doubt."

Figure 4 Evidence Data to Knowledge Conversion

This process models the data transition by requiring the inquirer to recognize the bias and prejudices they will be perceived to possess. Recognition of the inquirer's perceived associations to the evidence is essential in determining the meanings attributed to evidence interpretations. The purpose of establishing the inquirer's association to evidence is not to change the meanings attributed to evidence analysis but rather to better understand the reasoning processes that have lead to conclusions based on the analysis of evidence.

The purpose of modeling the transitional nature of data into evidence is to understand better how the evidence explains what occurred.

The evidence stakeholder perspective (illustrated in Figure 5) provides the mechanism for assessing the justification of a practitioner entering the enquiry and illustrates the practitioner's relationship to evidence. This facilitates a mechanism for determining bias and defines the extent of the practitioner's engagement in the enquiry process. The major contribution of this process is the explicit statement of association between enquirer and evidence.

As an inquirer may enter the inquiry process at any time during the process, their entry should be justifiable, having a legitimate reason for being granted access to the case evidence. Without a clear purpose for entering the inquiry process, access should be denied. Each entrant to the inquiry process will possess attributes deemed desirable that will contribute to drawing the case to a satisfactory conclusion.

Figure 5 Evidence Stakeholder Perspective

Stakeholder

Interpretation of Results

Stakeholder Evidence Management

Having been granted entry to an inquiry, the next step requires an explicit recognition of the bias and prejudices the entrant may be perceived to possess. The entrant will possess skills, knowledge, and qualifications considered worthy in furthering the progress of the inquiry but others may maintain an opinion as to how the entrant may conduct evidence analysis. As evidence may be defined as information possessing an ability to persuade, it is important to also understand the persuasive nature of the inquirer. The persuasive nature of the inquirer is directly associated with how others perceive them.

The next step in the inquiry process requires determining the purpose for which the entrant has been granted access to case evidence. The reason for entering the inquiry process designates the scope of conduct permitted to the inquirer. There are many reasons one may seek access to evidence, including: crime scene reconstruction based on forensic evidence, determining appropriate storage of evidence items, developing an evidence matrix for determining commonalities between witness statements, filing inquiry information, and determining appropriate methods of evidence analysis. The reason for limiting the scope of inquirer activity with the evidence is to assist in ensuring that the integrity of the evidence is not damaged during the progress of the investigation, and that the entrant only conducts those activities deemed necessary by their role.

Based on the entrant's skills, knowledge, and qualifications, together with a defined purpose, the inquirer may choose certain tools and techniques to apply to the evidence. It is important that the choice of tools and techniques are appropriate to the entrant's reason for accessing the evidence.

Once the preceding steps have been achieved to a level commensurate with the nature of the inquiry, the entrant may access the evidence. It is at this stage of the process that the inquirer shall conduct whatever examination of the evidence meets the specific needs of the inquiry. Following the examination and analyses of evidence, the results are produced, with such results varying dependent upon the nature of the examination process. Having obtained sets of analysis results, the inquirer sets about interpreting meanings to explain those particular aspects of the case being examined.

The final step in the inquiry process refers to evidence management. During a complex inquiry, there may be many subordinate inquiry processes, some conducted sequentially, others concurrent to the overall inquiry. Evidence management in this step relates only to the inquirer at hand and their management of the materials passing into their realm of responsibility. Most inquirers will only have access to small selections of the complete set of case related evidence. Having conducted their specific tasks with the evidence, the evidence continues along the inquiry process journey. Depending on the nature of the tasks conducted, the evidence may continue its journey, may have been subjected to destructive testing, or may transition into a case report.

The evidence relationships network (see Figure 6) process provides explanations for the linking relationships of categorized enquiry evidence discovered by practitioners when adopting a link perspective of evidence. As we tend to focus on what we can directly see, the major contribution of this process is directing the enquirer to examine the intangible links.

The purpose of this process is to understand the relationships between evidence, the inquiry domain, and other sets of information affecting evidence.

Figure 6 Evidence Relationships Network

Within the inquiry domain, certain common elements tend to be associated with an inquiry. The common elements are attributes associated with the incident, its location, the associated actors, and an offence. Evidence tends to be directly or indirectly linked to one or more of these four elements. This process draws the inquirer to identify the intangible links that exist between these four elements. The intangible links may exist between what, when, where, who, why, and how with incident, location, actor, and offence. The intangible links may relate to actions, inactions, ownership, possession, and knowledge of, or assist in explaining causes and effects.

The evidence network analysis (see Figure 7) process provides a network science perspective of an inquiry, thereby permitting visualizing the inquiry as an interrelated web and additionally providing a mathematical method for describing the relationships

Figure 7 Evidence Network Analysis

Evidence Analysis Interpretations

between evidence items. The major contribution of this process is the statistical analyses and visualizations of links and the absence of links that are enabled by adopting network science techniques.

The network science approach models objects in a defined situation as nodes, joined by links or relationships. A network consists of nodes linked to other nodes. Network science provides the underlying theory, tools, and techniques for determining the strength of nodes and links, and analyzes the changes in network structure and linkages in a dynamic situation. The importance of a node is measured according to a few simple rules. Determining the importance of networked nodes is achieved by examining centrality measures of degree, closeness, betweenness, and path length, in addition to overall network density. These measures indicate the strength of a node based on how well it is connected to the rest of the network.

Network science is used to analyze and visualize evidence relating to an inquiry. Plotting the evidence associated to a particular inquiry offers a perspective that may be focused on individual evidence items, or to a case as a whole. The network nodes are representations of individual evidence items, and, at finer levels of granularity, of evidence item attributes, while the links between nodes represent relationships. Network visualizations may be of specific moments frozen in time, or chained together to illustrate a dynamic situation as it evolves.

The evidence resource library (illustrated in Figure 8) facilitates practitioners proactively building and managing a repository of evidence-related resources. The major contribution of this process is being a living library of enquiry-related information.

As the scientific and legal efforts supporting forensic evidence continue to progress and develop, consolidation of resources enhances forensic evidence practitioner capabilities. To date much of the work conducted has been restricted to silos of expertise. The resource library models an approach to facilitate interactive multidisciplinary progress of evidence processes. It comprises both social and technological elements, presenting an extensive repository of data in the form of the evidence information system (EIS). The overall motivations of the stakeholders are represented by the top block above the EIS and forms the objectives. Data is contributed by the three stakeholder groups shown on the left-hand side of the EIS, with the action represented by the right-hand block, the project and process management. The technologies applied are shown in the lower block.

The participants interviewed across the three domains agreed that the evidence resource library was the most important component as well as the most difficult to develop as all stakeholder groups need to agree upon the foundation theories, standards, and ontologies. However, the development of such an integrated resource for evidence practitioners is considered an integral component to a holistic model for the tactical management of forensic evidence.

The evidence classification scheme (see Figure 9) facilitates the various procedural practices for classifying physical evidence items and, more particularly, classifying forensic evidence relationships. The major contribution of this process is providing a basic foundation for the identification, organization, and categorization of evidence at a global level, for application in law enforcement, forensic science and judicial domains. A complex inquiry is made up of diverse components. Apart from evidence associated with the case, there are people from different perspectives charged with undertaking different tasks. Each evidence practitioner, charged with different objectives to achieve, addresses evidence in a different manner. There is confusion arising from variations in terminologies and phrases applied to the same evidence. Legal requirements of evidence also vary between jurisdictions. This process presents a holistic approach to managing these diverse components.

Each evidence practitioner may require a system to organize the evidence set before them. Hence processes are defined to classify evidence items, and relationships between evidence items, according to the purpose of the inquiry.

The integration of the six processes presents a high-level meta-model for more effective handling of forensic evidence and its management across the three stakeholder domains. The meta-model exists only as a conceptual model as further analysis of component processes requires further detailed design before any prototype can be developed and tested in practice.

FORENSIC EVIDENCE MODEL EVALUATION

The building of the meta-model took place while interviews with the participants from the three stakeholder groups were in progress. This enabled a progressive development of processes to address problems and suggest potential solutions, moving between design of the new model, the underlying theories and considerations as to how it could be applied in practice. As the law enforcers were the drivers of the change, a focus group of law enforcement officers reviewed the meta-model and applied specific lower-level solutions to actual cases under investigation. A law enforcement focus group was chosen for the initial evaluation before progressing to the other two stakeholder groups. If the conceptual model cannot be applied in law enforcement, then no progression to the other stakeholder realms is justified. The focus group consisted of 10 law enforcement officers, each specializing in a different area and at varying levels of responsibility.

Earlier discussion in the forensic evidence problem space identified four broadly based local and global problems. Over one year, numerous situations were evaluated by the law enforcement focus group members; however, only a small portion of these implementations is reported in this discussion. Evaluation of the model by law enforcers has lead to many instances being suitable examples. These examples are taken from multiple international locations, but are considered to be representative of a local problem space.

Evaluation Example One

The identified problem was that there was no apparent formalized method or system for determining what the existence or nonexistence of evidence means to an investigation. A implementation of network science was applied to a cold case review instance. Instigating network science techniques raised a line of case-related questions regarding the existence of different evidence items, particularly in regard to information pertaining to bank account, cell phone, and family member contact activity currently as compared to previous periods, and that at the time of the initial investigation. Analysis of the dynamic network over time was necessary for an informed analysis of the evidence.

Practitioner responses included

• This approach, when compared with our traditional methods, has resulted in significant differences in understanding about the whole case and lead to renewed enthusiasm because of the new lines of enquiry offered. • The linking of evidence items and the absence of links provided direction for further investigation.

Evaluation Example Two

The identified problem was that investigators find that sorting and arranging forensic evidence in a meaningful manner is necessary yet impractical. A consideration of different stakeholder perspectives was needed. The model implemented showed that the researcher's association with the case evidence was different than that of investigating officers and that the detective has a different perspective than the police chief and other assisting officers. This implementation also highlighted that the purpose was to conduct a cold case review, examining the collected evidence, and asking questions about the evidence. The evidence had previously been collected and was assembled in one location and available for immediate examination and analysis. Those conducting the investigation were subject to limitations in that the evidence came to them in a piecemeal fashion, not in a sequential manner, and over different time periods. This caused the investigator to see the case evidence in small snapshots spread over a period of time in contrast to a situation where the evidence was available in its totality and sequentially arranged, offering a more holistic perspective.

This implementation facilitated assessment of a solution based on a specific rather than a general evidence classification.

Practitioner responses included

• Until exposed to this concept, evidence was just evidence and we had not thought about the character of evidence. • Evidence was always associated to a case and that was the end of the story.

• It was not that we did not do some of this stuff, it was just that we did not think about it nor fully understand our associations with the evidence.

Evaluation Example Three

The identified problem was that there is no apparent agreed method or system for describing or grouping types of relationships between evidence items. The network science process was undertaken, resulting in raising a line of case-related questions regarding evidence relationships. The problem relating to relationships pertained to current and previous activities of an actor in the investigation, highlighting the different types of relationships that could exist between things, between people, and between people and things bought new perspectives to the investigators. This process brought about an appreciation regarding evidence connectedness. The relationships between evidence can be mutual (that is, in both directions), asymmetrical (either inward to an evidence node or outward away from an evidence node), or null (signifying no relationship exists), leading investigators to realize another perspective regarding evidence interrelatedness. Another informal trial confirmed results of a previous evaluation (example one above), which illustrated the differences in approach between investigating officers.

Practitioner responses included

• The difference in approach results in significant differences in understanding the whole case. • The building of relationships between evidence items and between people and evidence items was improved and holistic views of the case were now possible.

Evaluation Example Four

The identified problem was that law enforcement officers were unaware of technology capacities because lack of financial support had lead to lack of technologyrelated training. The solution related to a specific and challenging instance. Use of a resource library system (limited in nature as compared to the theoretical model) showed that suitably arranged repositories of forensic evidence information can assist officers in resolving operational challenges. The demonstration assisted case resolution by taking paper-based GPS records and converting them into a digital format for storage and analysis in a database before plotting the recorded GPS coordinates onto a map, showing when and where a particular vehicle and person had traveled. This data was then able to be digitally compared with other information regarding mobile motor vehicle registration numbers stored in a computerized system.

Practitioner responses include

• This enabled us to visualize and link items of evidence from disparate sources.

• This shows interrelationships between different items of evidence not previously considered important.

The progressive nature of the movement between the problem space, theorizing about the design, and consolidating the design and application in a restricted event environment offered by design science provided a flexible approach for the research not available through other research methods.

LIMITATIONS

A major restriction in providing practicable solutions to the defined forensic evidence problem space is that the three stakeholder groups are not governed by an overarching body, so there is no direct enticement to view evidence holistically. With such a large space under consideration, it is difficult to employ and evaluate solutions in order to address the global problems identified.

Although design science provided a suitable mechanism for the research process, this method does not provide a formalized set of steps for conducting the work. New researchers applying design science may have difficulty estimating how far through the process they have progressed. In addition, design science has not yet addressed the handling of different perspectives, a necessity when dealing with domains involving complex human interactions.

CONCLUSION

The research at hand involved designing a model for the management of forensic evidence. Design science was used as the research method with mixed results. It allowed the researcher to get down and dirty at the operational level and readily move between theorizing and building. Although the iterative nature of design science provides the opportunity to immerse into the problem and solution spaces at the same time, at times it can be too flexible.

The models developed by the researcher in conjunction with the participants from the three stakeholder groups provide a holistic framework for effective management of forensic evidence. The implementation of such a high-level model across three domains is fraught with difficulty. Initial evaluation carried out by law enforcers provided positive feedback for specific models. Further research is needed for the detailed design of the component models and their implementation across the three domains. With regard to design science, research is also needed in complex human activity systems in order to provide guidance in the accommodation of different stakeholder perspectives.

Figure 1

 1 Figure 1 Iterative Approach Employed in the Research

Figure

  Figure 8 Evidence Resource Library


John Venable

Peter Newman

Nick Letch

Sue Ash

The Role of Public Policy in Enhancing the Design and Diffusion of Information Systems and Technology for Human Benefit

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Part 7: Panels of funding where sufficient return (profit) is not expected (or not returned soon enough), competitive forces leading to incompatibilities between different technologies (e.g., through product differentiation and creation of barriers to entry), and potential competition of new technologies for human benefit with established profit-making technologies. Barriers to adoption and diffusion of new technologies for human benefit include the expense and risk of new, possibly untried technologies, issues of organizational and social change, and lack of understanding of the role, purpose, potential benefits, and ways to obtain and use newly developed technologies.

Public policy has a key role to play in the development of new and adoption of new or existing technologies for human benefit. Governments and other policy development organizations may propose and implement public policy that provides funding or other incentives for development and adoption of technologies. Public policy may be used to set key priorities or technical directions or establish appropriate shared infrastructure. Public policy may regulate (or deregulate) how businesses or other organizations develop, deploy, or compete for and use new technologies to achieve improved human benefit. This panel will examine the role of public policy in encouraging the design, development, and adoption of new technologies, particularly information systems and technologies that have the goal of providing benefit to members of the public and humanity in general. Key areas and priorities for needed or changed public policy will be identified, together with recommendations for useful changes to public policy and how researchers may best engage in influencing public policy for human benefit.

THE ROLE OF PUBLIC POLICY IN ENHANCING THE DESIGN AND DIFFUSION OF INFORMATION SYSTEMS AND TECHNOLOGY FOR HUMAN BENEFIT

Technologies for human benefit, such as information systems and information technology, have a key role to play in the realization of quality of life for all citizenry by modern societies. New forms of IS and IT can be developed and used creatively to improve education, health, social equity, environmental conditions, social and environmental sustainability, government and not-for-profit services, participation in government, and enjoyment of life in general.

However, potentially valuable new technologies for human benefit may not be utilized due to barriers inherent in capitalist economies, including barriers to design and development of new technologies and barriers to adoption and diffusion of those new technologies. Some barriers to development stem from the profit motive, including lack


Thomas Chatain

Stefan Haar

Loïg Jezequel

Loïc Paulevé

Stefan Schwoon

Characterization of Reachable Attractors Using Petri Net Unfoldings

Keywords: dynamical systems, attractors, concurrency, qualitative models, biological networks

Attractors of network dynamics represent the long-term behaviours of the modelled system. Their characterization is therefore crucial for understanding the response and differentiation capabilities of a dynamical system. In the scope of qualitative models of interaction networks, the computation of attractors reachable from a given state of the network faces combinatorial issues due to the state space explosion. In this paper, we present a new algorithm that exploits the concurrency between transitions of parallel acting components in order to reduce the search space. The algorithm relies on Petri net unfoldings that can be used to compute a compact representation of the dynamics. We illustrate the applicability of the algorithm with Petri net models of cell signalling and regulation networks, Boolean and multi-valued. The proposed approach aims at being complementary to existing methods for deriving the attractors of Boolean models, while being generic since it applies to any safe Petri net.

Introduction

Living cells embed multiple regulation processes that lead to several emerging phenotypes such as cell differentiation, division, or response to environmental stress or signals. A large part of these processes are often represented as interaction networks (e.g., signalling networks, gene regulation networks) that describe the influences between numerous entities (genes, RNA, proteins). The global dynamics of such networks can then be captured using qualitative modelling frameworks, such as Boolean or discrete networks, that describe the possible transitions between the qualitative states of the system.

In the landscape of dynamics of a network model, one can distinguish between the transient and long-run dynamics, the latter being our focus in this article. In qualitative models, the long-run dynamics are referred to as attractors, and are formally defined as the Bottom Strongly Connected Components (BSCCs) of the transition graph whose nodes are the global states of the network, and directed edges are the possible direct transitions between those states. One typically distinguishes between two kind of attractors: the fixed points, that are the states from which no further transition is possible; and the cyclic attractors, that are a set of states that can be visited infinitely often.

Characterizing the attractors of network dynamics is key for capturing the potential adaptation and differentiation processes the cell can undergo. In particular, one could verify, from a given state of the network, if the dynamics always converges toward a unique attractor or may diverge towards different attractors. The former indicates a deterministic long-term behaviour, whereas the latter suggests an indeterministic differentiation, potentially controlled by additional mechanisms not captured by the level of abstraction of the model.

In practice, given a qualitative model of a network, the computation of the attractors reachable from one (set of) states can become very expensive as the size of the network grows. The naive approach consisting in generating the transition graph and computing the BSSCs suffers from the combinatorial explosion of the state space (exponential with the number of components of the network) and the explosion of the number of transitions.

A part of the combinatorial explosion of dynamics is due to the concurrency between the asynchronous transitions: in a given state, several transitions may be independently fired, which results in numerous redundant interleavings of transitions in the concrete transition space.

Contribution. In this paper, we propose a new algorithm for characterizing all the attractors that are reachable from a given initial state in a qualitative model expressed with safe Petri nets [START_REF] Murata | Petri nets: Properties, analysis and applications[END_REF], a broad class of nets which encompasses asynchronous Boolean or multi-valued networks. Our algorithm exploits the unfoldings of safe Petri net in order to reduce the size of the state space to explore.

Petri net unfoldings [START_REF] Esparza | Unfoldings -A Partial-Order Approach to Model Checking[END_REF][START_REF] Esparza | An improvement of McMillan's unfolding algorithm[END_REF] aim at representing the state space rechable from an initial state by exploiting concurrency between transitions to prune redundant interleavings of these transitions. To our knowledge this is the first algorithm for computing all the reachable attractors which relies on unfolding structures. Our algorithm is applicable to any safe Petri net.

Whereas experiments on particular cases of biological networks show room for improvement, such a technique exploiting concurrency is foremost complementary to existing algorithms (which ignore this dynamical feature) and therefore appeals for designing combinations of techniques to make tractable the analysis of very large networks.

Related work.

In the scope of Boolean networks, there has been numerous work to link the topology of the network (the interaction graph, giving signed relations between the components) with the fixed points -resulting in bounds or characterization of a subset of fixed points (e.g., [START_REF] Aracena | Maximum number of fixed points in regulatory boolean networks[END_REF][START_REF] Richard | Positive circuits and maximal number of fixed points in discrete dynamical systems[END_REF][START_REF] Paulevé | Topological Fixed Points in Boolean Networks[END_REF]); and with cyclic attractors, e.g., [START_REF] Richard | Negative circuits and sustained oscillations in asynchronous automata networks[END_REF][START_REF] Melliti | Full characterization of attractors for two intersected asynchronous boolean automata cycles[END_REF]. While the full characterization of the fixed points of Boolean/multivalued networks can be quite efficient for large networks [START_REF] Naldi | Decision diagrams for the representation and analysis of logical models of genetic networks[END_REF][START_REF] Paulevé | Refining dynamics of gene regulatory networks in a stochastic π-calculus framework[END_REF][START_REF] Hinkelmann | ADAM: Analysis of discrete models of biological systems using computer algebra[END_REF], the complete characterization of cyclic attractors is still a challenging task due to the combinatoric explosition of the state space to explore. Symbolic representation of the state space using binary decision diagrams has been used by [START_REF] Garg | Synchronous versus asynchronous modeling of gene regulatory networks[END_REF] to characterize attractors in synchronous and asynchronous Boolean networks. The relationships between attractors in synchronous and asynchronous settings has then been exploited in [START_REF] Berntenis | Detection of attractors of large boolean networks via exhaustive enumeration of appropriate subspaces of the state space[END_REF] to speed the exploration of all possible attractors in Boolean networks, as well as Boolean network reduction techniques in [START_REF] Zañudo | An effective network reduction approach to find the dynamical repertoire of discrete dynamic networks[END_REF]. Approximate methods are also largely considered, such as in [START_REF] Zheng | An efficient algorithm for computing attractors of synchronous and asynchronous boolean networks[END_REF], which selectively explore appropriate regions of the state space to derive a subset of cyclic attractors of the global network dynamics.

In this paper, we will focus on the use of unfolding to compute finite complete prefixes [START_REF] Khomenko | Canonical prefixes of Petri net unfoldings[END_REF] of safe Petri nets. Finite complete prefixes contain all the reachable markings in a compact representation (the prefix is always smaller than the reachability graph). Unfoldings are very well suited to capture concurrent system dynamics, and can be efficient for reachability analysis [START_REF] Esparza | Unfolding based algorithms for the reachability problem[END_REF], for instance.

Outline. In Sect. 2, we give a formal definition of (safe) Petri nets and their attractors, and introduce a running example. In Sect. 3, we present the unfolding of safe Petri nets. In Sect. 4, we detail our new algorithm to derive the attractors of a safe Petri net using its unfolding. Finally, implementation and experimations on Petri net models of biological networks are discussed in Sect. 5.

Petri Nets and Attractors

A Petri net is a bipartite graph where nodes are either places or transitions. In this paper, we consider only safe Petri nets where a place is either active or inactive (in oppositon to general Petri nets where each place can receive an arbitrary number of tokens, safe Petri nets allow at most one token per place). The set of active places form the state, or marking, of the net. A transition is said enabled if all the places that are parents of the transition are active. In the semantics, the firing of a transition makes inactive the parent places and then makes active the children places, modifying the current marking of the net.

Formally, a (safe) Petri net is a tuple N = P, T, F, M 0 where P and T are sets of nodes (called places and transitions respectively), and F ⊆ (P × T ) ∪ (T × P ) is a flow relation (whose elements are called arcs). A subset M ⊆ P of the places is called a marking, and M 0 = {p 1 0 , . . . , p n 0 } is a distinguished initial marking. For any node x ∈ P ∪ T , we call pre-set of x the set

• x = {y ∈ P ∪ T | (y, x) ∈ F } and post-set of x the set x • = {y ∈ P ∪ T | (x, y) ∈ F }.
A transition t ∈ T is enabled at a marking M if and only if • t ⊆ M . Then t can fire, leading to the new marking

M ′ = (M \ • t) ∪ t • . We write M t → M ′ . A firing sequence is a (finite or infinite) word w = t 1 t 2 . . . over T such that there exist markings M 1 , M 2 , . . . such that M 0 t1 → M 1 t2 → M 2 .
. . For any such firing sequence w, the markings M 1 , M 2 , . . . are called reachable markings.

The Petri nets we consider are said to be safe because we will assume that any reachable marking M is such that for any t ∈ T that can fire from M leading to M ′ , the following property holds: From an initial marking of the net, one can recursively derive all possible transitions and reachable markings, resulting in the marking graph (Def. 1). The marking graph is always finite in the case of safe Petri nets. The attractors reachable from the initial marking of the net can then be fully characterized by the bottom strongly connected components of the marking graph (Def. 2).

∀p ∈ M ∩ M ′ , p ∈ • t ∩ t • ∨ p / ∈ • t ∪ t • .

Definition 1 (Marking graph).

The marking graph of a Petri Net N is a directed graph G = (V, A) such that V is the set of all reachable markings (obtained from all the possible firing sequences) and

A ⊆ V × V is such that (M, M ′ ) ∈ A if and only if M t → M ′ for some t ∈ T .
Definition 2 (Attractors). An attractor is a bottom strongly connected component of G, that is a set A of markings such that either A = {M } and no transition is enabled from M ; or for every M ∈ A, the set of markings reachable from M is precisely A.

Unfoldings

In this section, we explain the basics of Petri net unfoldings. A more extensive treatment of the theory explained here can be found, e.g., in [START_REF] Esparza | Unfoldings -A Partial-Order Approach to Model Checking[END_REF]. Roughly speaking, the unfolding of a Petri net N is an "acyclic" Petri net U that has the same behaviours as N (modulo homomorphism). In general, U is an infinite net, but if N is safe, then it is possible [START_REF] Mcmillan | Using unfoldings to avoid the state explosion problem inthe verification of asynchronous circuits[END_REF] to compute a finite prefix P of U that is "complete" in the sense that every reachable marking of N has a reachable counterpart in P. Thus, P represents the set of reachable markings of N . Figure 2 shows a finite complete prefix of the unfolding of the Petri net of Figure 1. In principle, the set of reachable markings can also be computed by constructing the marking graph (see Definition 1). However, the marking graph suffers from combinatorial explosion due to concurrency. For instance, suppose that N simply contains n independent concurrent actions. Then the only attractor of the net is reached by executing all n actions in any arbitrary order. However, the marking graph will uselessly explore all n! different schedules for executing them, and all 2 n intermediate markings.

Research into concurrent systems has produced a number of solutions to alleviate the problem of combinatorial explosion due to concurrency (and eventually other sources). In [START_REF] Mcmillan | Using unfoldings to avoid the state explosion problem inthe verification of asynchronous circuits[END_REF], McMillan first proposed the use of finite unfolding prefixes. Esparza et al [START_REF] Esparza | An improvement of McMillan's unfolding algorithm[END_REF] later improved this solution. For instance, the unfolding of the previous example with n independent actions is simply of size O(n). With respect to the marking graph, an unfolding represents a time-space tradeoff: in general, a complete unfolding prefix P is much smaller than the marking graph of N , but the problem whether a marking M of N is reachable, given P, is NP-complete. However, this tradeoff is usually favourable [START_REF] Esparza | Unfolding based algorithms for the reachability problem[END_REF].

We now give some technical definitions to introduce unfoldings formally.

Definition 3 (Causality, conflict, concurrency). Let N = P, T, F, M 0 be a net and x, y ∈ P ∪ T two nodes of N . We say that x is a causal predecessor of y, noted x < y, if there exists a non-empty path of arcs from x to y. We note x ≤ y if x < y or x = y. If x ≤ y or y ≤ x, then x and y are said to be causally related.

x and y are in conflict, noted x # y, if there exist u, v ∈ T such that u ≤ x, v ≤ y, and

• u ∩ • v = ∅.
We call x and y concurrent, noted x co y, if they are neither causally related nor in conflict.

As we said before, an unfolding is an "acyclic" version of a net N . This notion of acyclicity is captured by Definition 4.

Definition 4 (Occurrence net). Let N = P, T, F, M 0 be a Petri net. We say that N is an occurrence net if it satisfies the following properties:

1. The causality relation < is acyclic; 2. | • p| ≤ 1 for all places p, and M (p) = 1 iff | • p| = 0; 3. for every transition t, t # t does not hold, and {x | x ≤ t} is finite.

As is convention in the unfolding literature, we shall refer to the places of an occurrence net as conditions and to its transitions as events. Due to the structural constraints, the firing sequences of occurrence nets have special properties: if some condition c is marked during a run, then the token on c was either present initially or produced by one particular event (the single event in • c); moreover, once the token on c is consumed, it can never be replaced by another token, due to the acyclicity constraint on <.

Definition 5 (Configuration, cut). Let N = C, E, F, M be an occurrence net. A set C ⊆ E is called configuration of N if (i) C is causally closed, i.e.
for all e, e ′ ∈ E with e ′ < e, if e ∈ C then e ′ ∈ C; and (ii) C is conflict-free, i.e. if e, e ′ ∈ C, then ¬(e # e ′ ). The cut of C, denoted Cut(C), is the set of conditions

(M ∪ C • ) \ • C.
Intuitively, a configuration is a set of events that can fire during a firing sequence of N , and its cut is the set of conditions marked after that firing sequence.

We can now define the notion of unfoldings. Let N = P, T, F, M 0 be a safe Petri net. The unfolding U = C, E, G, M ′ 0 of N is an (infinite) occurrence net (equipped with a homomorphism h) such that the firing sequences and reachable markings of U are exactly the firing sequences and reachable markings of N (modulo h). U can be inductively constructed as follows:

1. The conditions C are a subset of (E ∪ {⊥}) × P . For a condition c = x, p , we will have x = ⊥ iff x ∈ M ′ 0 ; otherwise x is the singleton event in • c. Moreover, h(c) = p. The initial marking M ′ 0 contains exactly one condition ⊥, p for each initially marked place p of N . 2. The events of E are a subset of 2 C × T . More precisely, we have an event e = C ′ , t for every set

C ′ ⊆ C such that c co c ′ holds for all c, c ′ ∈ C ′ and { h(c) | c ∈ C ′ } = • t.
In this case, we add edges c, e for each c ∈ C ′ (i.e.

• e = C ′ ), we set h(e) = t, and for each p ∈ t • , we add to C a condition c = e, p , connected by an edge e, c .

Intuitively, a condition x, p represents the possibility of putting a token onto place p through a particular firing sequence, while an event C ′ , t represents a possibility of firing transition t in a particular context. Recall that a configuration C of U represents a possible firing sequence, whose resulting marking corresponds, due to the construction of U , to a reachable marking of N . This marking is defined as

Mark (C) := { h(c) | c ∈ Cut(C) }.
Since U is infinite in general, we are interested in computing an initial portion of it (a prefix ) that completely characterizes the behaviour of N . is said to be a prefix of

U if E ′ ⊆ E is causally closed, C ′ = M ′ 0 ∪ E ′ •
, and G ′ is the restriction of G to C ′ and E ′ . A prefix P is said to be complete if for every reachable marking M of N there exists a configuration C of P such that (i) Mark (C) = M , and (ii) for each transition t ∈ T enabled in M , there is an event C ′′ , t ∈ E ′ enabled in Cut(C).

It is known [START_REF] Mcmillan | Using unfoldings to avoid the state explosion problem inthe verification of asynchronous circuits[END_REF][START_REF] Esparza | An improvement of McMillan's unfolding algorithm[END_REF] that the construction of such a complete prefix is indeed possible, and efficient tools [START_REF] Schwoon | Mole[END_REF][START_REF] Khomenko | Punf[END_REF] exist for this purpose. The precise details of this construction are out of scope for this paper; for what follows it suffices to know that it essentially follows the construction of U outlined above but that certain events are flagged as cut-offs when they do not "contribute any new reachable markings" (these events are represented by dashed lines in Figure 2). The construction then does not continue "beyond" such a cut-off event.

Extracting attractors from unfoldings

Our method for finding the attractors of a Petri net N uses unfoldings in two steps: first to find a set of markings which intersects all the attractors, second to output the attractors as a set of finite complete prefixes.

Representation of attractors as finite complete prefixes

We first remark that finite complete prefixes of unfoldings are particularly well suited for the representation of attractors. In fact, every attractor A is a set of states which form a maximal strongly connected component of the marking graph of N . For every marking M in A, the attractor A is precisely the set of markings reachable from M . Hence it can be compactly represented as a finite complete prefix of the unfolding of the Petri net N initialized at M . Denote this prefix U M : the markings associated to the configurations of U M are precisely those of the attractor, moreover the prefix shows the dynamics of the net while in the attractor. Last, the size of U M (as number of non cut-off events) can be up to exponentially smaller (in case of highly concurrent behaviour) than the number of markings in the attractor, and never exceeds it.

Figure 3 shows two attractors of the Petri net N of Figure 1 represented as finite complete prefixes. The one on the left, U {p4,p6} , represents the attractor containing the marking {p 4 , p 6 }. The one on the right represents the attractor made of the single marking {p 3 , p 2 } which is a deadlock.

Maximal configurations and attractors

We have shown the interest of prefixes for representing attractors. What we need is a way to find a set M of markings of the Petri net N which contains one marking per attractor. Given such M, the set {U M | M ∈ M} gives a complete characterization of the attractors of N . Now we show that the desired set M of markings can be obtained from the maximal configurations of a finite complete prefix of the unfolding of N .

Definition 7 (maximal configuration).

A configuration of a prefix is called maximal if no other event of the prefix can be added to the configuration. Equivalently, the configuration is a deadlock of the prefix viewed as a Petri net.

For example, in the prefix shown on Figure 2, the configuration corresponding to the firing sequence t 3 t 2 is not maximal because it can be extended, for instance by t 4 and the other event labeled t 3 , yielding this time a maximal configuration, which reaches the marking {p 4 , p 5 }. Notice that this marking is not a deadlock in the original Petri net, yet the configuration is maximal in the prefix.

Property 1. Let N be a Petri net and U a finite complete prefix of its unfolding. For every attractor A of N , there exists a maximal configuration of U whose associated marking belongs to A.

Proof. Choose a marking M in A. Because U is complete, it has a configuration C whose associated marking is M . Now because U is finite, it has a maximal configuration C ′ which extends C. The marking M ′ associated to C ′ is reachable from M , therefore it is also in A.

The prefix shown on Figure 2 has four maximal configurations. One is obtained after firing only t 1 ; its associated marking is the deadlock {p 3 , p 2 }. This marking is associated to another maximal configuration: the one obtained by firing t 3 and then t 2 t 1 concurrently with t 4 . The third maximal configurations is obtained by firing t 3 , then t 2 and t 4 concurrently, and then t 3 again; it reaches the marking {p 4 , p 5 }. Finally, one can fire t 3 , then t 2 t 1 and t 6 concurrently, and then t 5 ; it reaches the marking {p 4 , p 6 }.

One can check that every attractor has a marking in this set: the deadlock {p 3 , p 2 } is represented twice; the marking {p 4 , p 6 } represents the attractor {{p 3 , p 6 }, {p 1 , p 6 }, {p 4 , p 6 }}. The marking {p 4 , p 5 }, also associated to a maximal configuration of U , is not in an attractor.

Algorithm

Property 1 allows one to use finite complete prefixes to identify attractors: the set M max of markings corresponding to maximal configurations intersects all the attractors. But not all the markings in M max belong to an attractor. Also an attractor may contain several markings in M max .

In order to characterize the attractors of a safe Petri net N , we filter the set M max and keep only one marking per attractor. The idea is to remove iteratively the markings from which another marking of the set is reachable. The reachability checking is done again using unfoldings.

The algorithm is the following:

1. Compute a finite complete prefix U of the unfolding of N .

2. Initialize M to the set M max of markings corresponding to maximal configurations of U . 3. Initialize the set of attractors to ∅.

Loop for M in M

-Compute a finite complete prefix U M of the net N initialized at M .

-If a marking M ′ ∈ M other than M is reachable from M (the reachability check is done using U M ), Then remove M from M, Else add U M to the set of attractors. 5. Output the set of attractors.

Termination of the algorithm is straightforward. We prove that at every step of the algorithm, the set M intersects all the attractors. This property is preserved when we remove a marking M from M because, if M is in an attractor A, then the marking M ′ ∈ M reachable from M is also in A. Notice also that, if M is not in an attractor, then at least one attractor A is reachable from M ; and because M ∩ A = ∅, M contains a marking M ′ ∈ A which is reachable from M . This ensures that U M is added to the set of attractors iff M is in an attractor A and M ∩ A = {M }.

Illustration on the running example

For our running example the set M is initialized to {{p 3 , p 2 }, {p 4 , p 5 }, {p 4 , p 6 }}. The algorithm computes the prefix U M for every M ∈ M, but outputs only U {p3,p2} and U {p4,p6} , pictured in Figure 3. U {p4,p5} is dropped because {p 4 , p 6 } is reachable from {p 4 , p 5 }.

Implementation and Experimental Results

In order to test the applicability of our approach, we implemented a prototype of the algorithm described above using Mole [START_REF] Schwoon | Mole[END_REF] for computing the complete prefixes, and Minisat [START_REF] Eén | An extensible sat-solver[END_REF] for extracting the maximal configurations 4 .

We applied our algorithm for the identification of attractors of three qualitative models of biological networks taken from the literature. In all cases, we applied a transformation to safe Petri net (Appendix A) that consists in having one place for each qualitative level of each component of the network, and transitions corresponding to the asynchronous semantics, i.e., each transition will actually change the level of only one component. By construction, the places corresponding to the levels of each components are mutually exclusive. The initial marking may then correspond either to a single state of the qualitative model, or to several possible initial states by adding transitions that non-deterministically select the initial state for some components (Sect. A.2). In this latter encoding, the returned attractors are the attractors reachable from at least one of the possible initial state of the qualitative model. 1. Results of the attractors characterization using Petri net unfoldings. For each model (which includes the initial state), we give the number of maximal configurations and the number of attractors reachable from the initial state.

Tab. 1 sums up the results of computing the finite complete prefixes on the following regulatory networks: a multi-valued model of the lambda switch [START_REF] Thieffry | Dynamical behaviour of biological regulatory networks -II. Immunity control in bacteriophage lambda[END_REF], a Boolean model of he mammalian cell cycle [START_REF] Faure | Dynamical analysis of a generic Boolean model for the control of the mammalian cell cycle[END_REF], a Boolean model of the ERBB receptor [START_REF] Sahin | Modeling ERBB receptor-regulated G1/S transition to find novel targets for de novo trastuzumab resistance[END_REF], and a multi-valued model of fate determination in the Vulval Precursor Cells (VPC) in C. elegans [START_REF] Weinstein | A network model for the specification of vulval precursor cells and cell fusion control in caenorhabditis elegans[END_REF]. For the ERBB model, two different initial settings have been tested: (1) when EGF is active; (2) when either EGF is active or inactive. For the other models, the initial state is the level 0 for all the components. The execution times are in the order of a fraction of a second for the two first models; in the order of a few seconds for ERBB; and around 15 minutes for the VPC model. For the latter, we note that starting from a different initial state leads to a combinatoric explosion of the complete prefix, showing room for improvement to handle large model in general. It is difficult to compare with other existing tools as most of them handle only Boolean networks and do not support the search from a given initial state. GINsim [START_REF] Naldi | Logical modelling of regulatory networks with GINsim[END_REF] also provides attractors computations from a given initial state, but it relies on explicit state transition graph computation, which is always larger than a complete prefix (Section 3). For instance on the VPC example, GINsim has been stopped after one hour.

Discussion

We presented a new algorithm for computing all the attractors reachable from a given state in the general class of safe Petri nets, i.e., Petri nets having at most one token in each place. This class includes Boolean and multi-valued networks that are typically used to model the qualitative dynamics of biological networks.

Our approach relies on Petri net unfoldings that natively take into account the concurrency between transitions to produce a compact representation of the reachable states. Then, we use the notion of maximal configuration to derive, from the computed unfolding, a set of states that includes at least one state of each reachable attractor. This set of maximal configuration is then filtered to output exactly one state per reachable attractors. The identification of attractors is complete in the sense that all the attractors reachable from the supplied markings are detected, including fixed points and cyclic and complex attractors.

By the use of Petri unfoldings, we aim at reducing the complexity of exploring the full reachable space by inherently pruning redundant transitions due to some interleaving of concurrent transitions. We applied a prototype implementation of the algorithm to four biological networks ranging from four to eighty interacting components, either multi-valued or Boolean.

The unfolding technique mentioned in this paper is generic to any safe Petri net. This indicates several directions for improving its computation (including the extraction of maximal configurations) in the particular case of biological interaction networks, such as the use of contextual Petri nets [START_REF] Baldan | Efficient unfolding of contextual Petri nets[END_REF], merge processes [START_REF] Khomenko | An algorithm for direct construction of complete merged processes[END_REF], unravelings [START_REF] Casu | Flow unfolding of safe nets[END_REF], and the use of the network topology and static analysis to prune non-necessary transitions and decompose the detection of attractors.

A Encoding asynchronous discrete networks with safe Petri Nets

A.1 Encoding with one initial state

In literature, Boolean and multi-valued networks modelling dynamics of biological influence networks are typically represented by functions associating for each component the levels towards which it evolves with respect to each possible level of its regulators. In order to encode their asynchronous dynamics in Petri nets, one need to have a transition-centered representation, instead of a function-centered. Informally, this can be achieved by having one place per possible level of each component (we note i u the place corresponding to the level u of component i), and listing the conditions for moving a token from i u to i u+1 and i u-1 . Such conditions can typically be built from the expression of the discrete functions of the network. Our encoding always results in safe Petri nets, which makes it different from [START_REF] Chaouiya | Petri net representation of multi-valued logical regulatory graphs[END_REF] which relies on more advanced Petri nets semantics (multiple tokens on places and weighted arcs), A Discrete Network gathers a finite number of components i ∈ {1, • • • , n} having a discrete finite domain F i that we note

F i = {0, • • • , l i }, l i being the maximum level for the component i. For each component i ∈ {1, • • • , n}, a map f i : F → F i is defined, where F = F 1 × • • • × F n ,
giving the next value of the component with respect to the global state of the network. Typically f i depends on a subset of components (its regulators) that we denote dep(f i ). In the case of Asynchronous Discrete Networks (ADN), a transition relation

→ ADN ⊆ F × F is defined such that x → ADN x ′ if and only if there exists a unique i ∈ {1, • • • , n} such that x ′ [i] = f i (x) and ∀j ∈ {1, • • • , n}, j = i, x ′ [j] = x[j],
i.e. one and only one component has been updated. This is formalised in Def. 8.

Definition 8 (Asynchronous Discrete Network (ADN)

). An ADN is defined by a couple (F, f 1 , . . . , f n ) where F = F 1 × • • • × F n , and ∀i ∈ {1, • • • , n}, f i : F → F i with F i = {0, • • • , l i }. Given two states x, x ′ ∈ F, the transition relation → ADN is given by

x → ADN x ′ ⇐⇒ ∃i ∈ {1, • • • , n}, f i (x) = x ′ [i]∧∀j ∈ {1, • • • , n}, j = i, x[j] = x ′ [j] ,
where x[i] is the i-th component of x. We note dep(f i ) ⊆ {1, • • • , n} the set of components on which the value of f i depends: ∀x, x ′ ∈ F such that ∀j ∈ dep(f i ), x[j] = x ′ [j], necessarily f i (x) = f i (x ′ ).

In the scope of an ADN (F, f 1 , . . . , f n ), we use cond(x) to map a state to the set of literals for the presence of the components at the corresponding state, e.g., cond( 1, 0, 1 ) = {1 1 , 2 0 , 3 1 }: cond(x)

∆ = {i u | i ∈ {1, • • • , n}, x[i] = u}.
Given a component i at a state u, we note conds i u+ and conds i u-the set of conditions where i can respectively increase or decrease. This set of conditions can be read as a disjunctive normal form expressing the possibility of the transition: conds i Finally, given an ADN (F, f 1 , . . . , f n ) and an initial state x 0 ∈ F, the corresponding safe Petri net is defined by (P, T, F, M 0 ) where P = {i u | i ∈ {1, • • • , n}, u ∈ {0, • • • , l i }}, M 0 = cond(x 0 ), and T and F are the smallest sets (w.r.t. inclusion) such that ∀i ∈ {1, • • • , n}, ∀u ∈ {0, • • • , l i }, ∀Φ ∈ conds i u+ ∪ conds i u-, ∃t ∈ T : • t = Φ ∪ {a i } ∧ t • = (Φ \ {a i }) ∪ {a j }. By construction, the Petri net is safe and for each i ∈ {1, • • • , n}, the places i 0 , • • • , i li are mutually exclusive.

A.2 Encoding with multiple initial states

When studying the dynamics of a qualitative network, one may want to consider several initial states, chosen nondeterministically. Using the construction depicted in the previous section, one can encode this indeterministic choice by adding a place, initially marked, per (independent) indeterministic choice, and a transition per corresponding (local) state. Fig. 4 illustrate this construction with either an indeterministic initial state for one component, or for several components.

Fig. 1 .

 1 Fig. 1. A safe Petri net (left) and the corresponding marking graph (right) -the initial marking is in bold.

Figure 1 (

 1 Figure 1 (left) shows an example of a safe Petri net. The places are represented by circles and the transitions by horizontal lines (each one with a label identifying it). The arrows represent the arcs. The initial marking is represented by dots (or tokens) in the marked places.From an initial marking of the net, one can recursively derive all possible transitions and reachable markings, resulting in the marking graph (Def. 1). The marking graph is always finite in the case of safe Petri nets. The attractors reachable from the initial marking of the net can then be fully characterized by the bottom strongly connected components of the marking graph (Def. 2).

Figure 1 (

 1 Figure 1 (right) represents the marking graph of the Petri net of Figure 1 (left). The two attractors of the Petri net of Figure 1 (left) are evidenced by the grey parts of its marking graph in Figure 1 (right).

  p

Fig. 2 .

 2 Fig. 2. A finite complete prefix of the unfolding of the Petri net of Figure 1. Dashed events are flagged as cut-offs: the unfolding procedure does not continue beyond them.

Definition 6 ( 3 Fig. 3 .

 633 Fig. 3. Two attractors of the Petri net of Figure 1 represented as finite complete prefixes U {p 4 ,p 6 } (on the left) and U {p 3 ,p 2 } (on the right).

==

  simplify({cond(x)| dep(i) | x ∈ F, x[i] = u, f i (x) > u}); simplify({cond(x)| dep(i) | x ∈ F, x[i] = u, f i (x) < u});where simplify is an operator to reduce the number of conditions, and cond(x)| dep(i) restricts the literals to those corresponding to components influencing i.

Fig. 4 .

 4 Fig. 4. (left) Encoding of the indeterministic choice between the initial state of 1; (right) indeterministic choice between the initial state of the couple 1 and 2: either 0, 0 or 1, 1 .

Executables, scripts, and Petri net models are available for Linux 64bits at http://loicpauleve.name/cmsb2014.tbz2