We define extensions of CTL and TCTL with strategic operators, called Strategic CTL (SCTL) and Strategic TCTL (STCTL), respectively. For each of the above logics we give a synchronous and asynchronous semantics, ie STCTL is interpreted over networks of extended Timed Automata (TA) that either make synchronous moves or synchronise via joint actions. We consider several semantics regarding information: imperfect (i) and perfect (I), and recall: imperfect (r) and perfect (R). We prove that SCTL is more expressive than ATL for all semantics, and this holds for the timed versions as well. Moreover, the model checking problem for STCTLir is of the same complexity as for ATLir, the model checking problem for STCTLir is of the same complexity as for TCTL, while for STCTLiR it is undecidable as for ATLiR. The above results suggest to use STCTLir and STCTLir in practical applications. Therefore, we use the tool IMITATOR to support model checking of STCTLir.

International audience

Abstract Reaction systems are a model of computation inspired by the biochemistry exhibited by living cells. This paper introduces the notion of agency as an extension to the reaction systems formalism, leading to distributed reaction systems. Adding agents in the reaction systems setting, allows for the natural modelling and representation of multi-agent and distributed systems. To support the specification of temporal-epistemic properties of distributed reaction systems, we introduce the logic rs ctlk and present experimental results of its associated model checking procedure run on a biological benchmark of within-cell signal transduction networks. The experimental results are encouraging despite the complexity of the rs ctlk model checking problem that is shown to be pspace -complete.

Strategic Timed CTL (STCTL) is an expressive logic that integrates branching time CTL with the representation of continuous time, and the notion of strategic abilities of agents. This makes STCTL suitable for specifying properties of asynchronous multi-agent systems modeled as networks of Parametric Timed Automata (PTA). Existing model checkers and synthesis procedures for STCTL are often limited in scope (bounded analyses), rely on ad-hoc implementations, and are difficult to prove correct. In this paper we propose declarative methods for STCTL model checking and synthesis using rewriting logic. Our approach uses rewriting modulo SMT to represent clock constraints and timed parameters as terms in a rewrite theory, and we adequately capture the continuous semantics of STCTL via rewriting strategies. The resulting algebraic specification is executable in the rewrite engine Maude. This is a novel application of Maude’s strategy language and, since our procedures are grounded on logical means, it is simpler to prove them correct. Our approach advances the state of the art for the analysis of multi-agent systems by allowing for the nesting of temporal operators and universal STCTL formulas, which have not been considered before. We benchmark our rewrite theory against existing procedures for STCTL, demonstrating competitive performance and even outperforming dedicated procedures for the existential fragment of STCTL. We thus provide a more robust and verifiable approach to STCTL model checking and synthesis.

Abstract Reaction systems are a formal model for computational processing in which reactions operate on sets of entities (molecules) providing a framework for dealing with qualitative aspects of biochemical systems. This paper is concerned with reaction systems in which entities can have discrete concentrations, and so reactions operate on multisets rather than sets of entities. The resulting framework allows one to deal with quantitative aspects of reaction systems, and a bespoke linear-time temporal logic allows one to express and verify a wide range of key behavioural system properties. In practical applications, a reaction system with discrete concentrations may only be partially specified, and the possibility of an effective automated calculation of the missing details provides an attractive design approach. With this idea in mind, the current paper discusses parametric reaction systems with parameters representing unknown parts of hypothetical reactions. The main result is a method aimed at replacing the parameters in such a way that the resulting reaction system operating in a specified external environment satisfies a given temporal logic formula.This paper provides an encoding of parametric reaction systems in smt , and outlines a synthesis procedure based on bounded model checking for solving the synthesis problem. It also reports on the initial experimental results demonstrating the feasibility of the novel synthesis method.

Expressing attack-defence trees in a multiagent setting allows for studying a new aspect of security scenarios, namely, how the number of agents and their task assignment impact the performance,e.g.,attack time, of strategies executed by opposing coalitions. Optimal scheduling of agents' actions, a nontrivial problem, is thus vital. We discuss associated caveats and propose an algorithm that synthesizes such an assignment, targeting minimal attack time and using the minimal number of agents for a given attack-defence tree. We also investigate an alternative approach for the same problem using rewriting logic, starting with a simple and elegant declarative model, whose correctness (in terms of schedule's optimality) is self-evident. We then refine this specification, inspired by the design of our specialized algorithm, to obtain an efficient system that can be used as a playground to explore various aspects of attack-defence trees. We compare the two approaches on different benchmarks.

The paper presents a novel SMT-based method for testing the satisfiability of formulae that express strategic properties of timed multi-agent systems represented by networks of timed automata. Strategic Metric Temporal Logic (SMTL) is introduced, which extends Metric Temporal Logic (MTL) with strategy operators. SMTL is interpreted over maximal continuous time runs of timed automata. We define a procedure that synthesises a model for a given SMTL formula if such a model exists. The method exploits Satisfiability Modulo Theories (SMT) techniques and Parametric Bounded Model Checking algorithms. The presented approach enables bounded satisfiability checking, where the model is partially given and needs to be completed in line with the given specification. Our method has been implemented, and its application is demonstrated through an example of the well-known dining philosophers problem extended with clocks and strategies. The experimental results are quite encouraging.

Expressing attack-defence trees in a multi-agent setting allows for studying a new aspect of security scenarios, namely how the number of agents and their task assignment impact the performance, e.g. attack time, of strategies executed by opposing coalitions. Optimal scheduling of agents' actions, a non-trivial problem, is thus vital. We discuss associated caveats and propose an algorithm that synthesises such an assignment, targeting minimal attack time and using minimal number of agents for a given attack-defence tree.

Recently, we have proposed a framework for verification of agents' abilities in asynchronous multi-agent systems (MAS), together with an algorithm for automated reduction of models. The semantics was built on the modeling tradition of distributed systems. As we show here, this can sometimes lead to counterintuitive interpretation of formulas when reasoning about the outcome of strategies. First, the semantics disregards finite paths, and yields unnatural evaluation of strategies with deadlocks. Secondly, the semantic representations do not allow to capture the asymmetry between proactive agents and the recipients of their choices. We propose how to avoid the problems by a suitable extension of the representations and change of the execution semantics for asynchronous MAS. We also prove that the model reduction scheme still works in the modified framework.

In this paper, we introduce a new method of the satisfiability (SAT) checking for Simple-Goal Strategy Logic (SL[SG]), using symbolic Boolean model encoding and the SAT Modulo Monotonic Theories techniques, which was implemented into the tool SGSAT. To the best of our knowledge, this is the only tool solving the SAT problem for SL[SG]. Its applications include process synthesis, developing controllers as well as automatic planners in multi-agent scenarios.

co-located with the 40th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2019).Both conferences were organized by the Process and

This special issue contains articles selected from CS&P 2018, the 27th Workshop on Concurrency, Specification, and Programming.CS&P deals with formal specification of concurrent and parallel systems, mathematical models for describing such systems, and programming and verification concepts for their implementation.The workshop is one of a series of events organised every even year by Humboldt University of Berlin and every odd year by Warsaw University.Dating back to the midseventies, CS&P has become an important forum for researchers from European and Asian countries.CS&P 2018 was held at Humboldt University Berlin-Adlershof, Germany, in September 24-26, 2018, and featured 20 papers accepted for presentation by the program committee.After the conference, six outstanding papers were selected by the Steering Committee based on the previous reviews and the quality of the presentations.Their authors were given time to integrate the reviewer's and audience's feedback, as well as to substantially improve and extend their contributions.After the second round of reviewing by additional experts, during the pandemic year of 2020 the authors polished and finalized their contributions, to yield the mature articles which can be found in this special issue.

Synthesis of models and strategies is a very important task in software engineering. The main problem here consists in checking the satisfiability of formulae expressing the specification of a system to be implemented. This paper puts forward a novel method for deciding the satisfiability of formulae of Alternating-time Temporal Logic (ATL) under perfect and imperfect information. The synthesised models of strategic games are often minimal. The method expands the one for CTL exploiting SAT Modulo Monotonic Theories (SMMT) solvers. Our tool MsATL combines SMMT solvers with two existing ATL model checkers: MCMAS and STV. This is the first ever tool for checking the satisfiability of imperfect information ATL. The experimental results show that, similarly to the CTL case, our approach appears to be very efficient and can quickly check the satisfiability of large ATL formulae that have been out of reach of the existing approaches.

Some multi-agent scenarios call for the possibility of evaluating specifications in a richer domain of truth values. Examples include runtime monitoring of a temporal property over a growing prefix of an infinite path, inconsistency analysis in distributed databases, and verification methods that use incomplete anytime algorithms, such as bounded model checking. In this paper, we present multi-valued alternating-time temporal logic ( mv-ATL → ∗ ), an expressive logic to specify strategic abilities in multi-agent systems. It is well known that, for branchingtime logics, a general method for model-independent translation from multi-valued to two-valued model checking exists. We show that the method cannot be directly extended to mv-ATL → ∗ . We also propose two ways of overcoming the problem. Firstly, we identify constraints on formulas for which the model-independent translation can be suitably adapted. Secondly, we present a model-dependent reduction that can be applied to all formulas of mv-ATL → ∗ . We show that, in all cases, the complexity of verification increases only linearly when new truth values are added to the evaluation domain. We also consider several examples that show possible applications of mv-ATL → ∗ and motivate its use for model checking multi-agent systems.

We propose a general semantics for strategic abilities of agents in asynchronous systems, with and without perfect information. Based on the semantics, we show some general complexity results for verification of strategic abilities in asynchronous interaction. More importantly, we develop a methodology for partial order reduction in verification of agents with imperfect information. We show that the reduction preserves an important subset of strategic properties, with as well as without the fairness assumption. We also demonstrate the effectiveness of the reduction on a number of benchmarks. Interestingly, the reduction does not work for strategic abilities under perfect information.

In earlier work, we presented translations of attack-defence trees (ADTrees) to extended asynchronous multi-agent systems. By avoiding some sequences, agent models constructed via these transformations already embed state space reductions. Here, we introduce Guarded Update Systems and their synchronisation topology, allowing us to define a new general reduction scheme that applies to tree topologies, and in particular to ADTrees. The reduction exploits the layered structure of a tree by avoiding unnecessary interleavings between nodes at different depths. We prove the soundness of this new method and present extensive experimental results, including scalable models, to demonstrate it can be effectively used alongside previously employed techniques.

This special issue is based on extended versions of the best papers presented at the 39th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2018).Petri Nets 2018 was co-located with the Application of Concurrency to System Design Conference (ACSD 2018).Both were organized by the Interes Institute and Faculty of Electrical Engineering and Information Technology, Slovak University of Technology.The conference took place at the Austria Trend Hotel Bratislava, from June 24 to June 29, 2018.In total, 33 papers were submitted to Petri Nets 2018 by authors from 19 different countries.Each paper was reviewed by three reviewers.The Program Committee (PC) selected 23 papers for presentation: 15 theory papers and 8 tool papers.The authors of the best six papers were invited to submit an extended version of their conference paper for this special issue.The selected papers contained highly innovative and very strong contributions, as was demonstrated by the unanimous support of the reviewers.Also the PC unanimously supported these invitations.After a rigorous review process comprising two rounds of reviewing, the invited papers were accepted.Besides a subset of the original reviewers, we also invited additional reviewers to ensure the best feedback possible.We believe that the papers in this special issue are of high quality and represent the state-of-the-art in their respective fields.The article "Analysis and Synthesis of Weighted Marked Graph Petri Nets" by Raymond Devillers and Thomas Hujsa focuses on an important subclass of persistent Petri nets, the weighted marked graphs (WMGs), also called generalised (or weighted) event (or marked) graphs or weighted T-nets.The authors provide new behavioural properties of WMGs expressed on their reachability graph, notably backward persistence and strong similarities between any two sequences sharing the same starting state and the same destination state.They also propose necessary structural conditions that must be fulfilled by a labelled transition system to be WMG-solvable.Finally, the authors propose a general synthesis method to create a WMG whose reachability graph minimally includes the specification.The article "Operational Semantics, Interval Orders and Sequences of Antichains" by Ryszard Janicki and Maciej Koutny introduces a new general class of nets that can represent both inhibitor and activator nets -called safe nets with context arcs.The authors analyse in detail fundamental relationships between interval sequences and sequences of maximal antichains, and provide simple algorithms that transform one into another.

We present nine SAT-solvers and compare their efficiency for several decision and combinatorial problems: three classical NP-complete problems of the graph theory, bounded Post correspondence problem (BPCP), extended string correction problem (ESCP), two popular chess problems, PSPACE-complete veri fication of UML systems, and the Towers of Hanoi (ToH) of exponential solutions. In addition to several known reductions to SAT for the problems of graph k-colouring, vertex k-cover, Hamiltonian path, and verification of UML systems, we also define new original reductions for the N-queens problem, the knight’s tour problem, and ToH, SCP, and BPCP. Our extensive experimental results allow for drawing quite interesting conclusions on efficiency and applicability of SAT-solvers to different problems: they behave quite efficiently for NP-complete and harder problems but they are by far inferior to tailored algorithms for specific problems of lower complexity.

This special issue of Fundamenta Informaticae is dedicated to papers selected from the 26 th International Workshop on CONCURRENCY, SPECIFICATION, AND PROGRAMMING (CS&P 2017), which took place in Warsaw, Poland, in

In this paper we investigate the Timed Alternating-Time Temporal Logic (TATL), a discrete-time extension of ATL. In particular, we propose, systematize, and further study semantic variants of TATL, based on different notions of a strategy. The notions are derived from different assumptions about the agents’ memory and observational capabilities, and range from timed perfect recall to untimed memoryless plans. We also introduce a new semantics based on counting the number of visits to locations during the play. We show that all the semantics, except for the untimed memoryless one, are equivalent when punctuality constraints are not allowed in the formulae. In fact, abilities in all those notions of a strategy collapse to the “counting” semantics with only two actions allowed per location. On the other hand, this simple pattern does not extend to the full TATL. As a consequence, we establish a hierarchy of TATL semantics, based on the expressivity of the underlying strategies, and we show when some of the semantics coincide. In particular, we prove that more compact representations are possible for a reasonable subset of TATL specifications, which should improve the efficiency of model checking and strategy synthesis.

took place at the School of Engineering and Architecture of Zaragoza University from June 25 to June 30, 2017.

We present the web service composition system TripICS, which allows for an easy and user-friendly planning of visits to interesting cities and places around the world in combination with travels, arranged in the way satisfying the user’s requirements. TripICS is a specialization of the concrete pla nning of PlanICS viewed as a constrained optimization problem to the ontology containing services provided by hotels, airlines, railways, museums etc. The system finds an optimal plan by applying a modification of the most efficient concrete planner of PlanICS based on a combination of an SMT-solver with the algorithm GEO. The modification has been designed in order to solve quickly multiple equality constraints. The efficiency of the new planning algorithm is proved by experimental results.

Reaction systems are a formal model for computational processes inspired by the functioning of the living cell. This paper introduces reaction systems with discrete concentrations, which are an extension of reaction systems allowing for quantitative modelling. We demonstrate that although reaction systems with discrete concentrations are semantically equivalent to the original qualitative reaction systems, they provide much more succinct representations in terms of the number of entities being used. We define a variant of Linear Time Temporal Logic interpreted over models of reaction systems with discrete concentrations. We provide its suitable encoding in SMT, together with bounded model checking, and present experimental results demonstrating the scalability of the verification method for reaction systems with discrete concentrations.

This is the seventeenth special issue of Fundamenta Informaticae based on the CONCURRENCY SPECIFICATION AND PROGRAMMING (CS&P) workshop, in succession to the sixteenth special issue published in 2014.The CS&P workshops, being held every even year in Germany and every odd year in Poland, take place on the basis of an exchange programme between University of Warsaw and Humboldt University in Berlin.Initiated by computer science and mathematical logic interest groups affiliated to Warsaw and Humboldt Universities in the mid-seventies of the XX century, the workshops were suspended for some years in the eighties and resumed in 1992 in the extended form of participation: they evolved from bilateral meetings to the meetings hosting researchers also from a number of countries other than Germany and Poland.The scope of subjects has been broadened too: from linguistic and logical issues initially to diverse research areas such as, for instance, the aforesaid ones.This part contains selected and extended versions of 11 out of 32 articles presented at the meeting that took place in Chemnitz from September 29 to October 1, 2014.As it was the case of all the previous special issues of Fundamenta Informaticae based on CS&P, the articles were selected on the basis of a review process admitted by international scientific periodicals.A complete collection of the contributions has been edited by Louchka Popova-Zeugmann and Holger Schlingloff of Humboldt University and Matthias Werner of Technical University, Chemnitz and published before the workshop as Proceedings.This is, thus, a continuation of the tradition of the former CS&Ps, whose participants had been supplied with proceedings in the form of technical reports during the meetings.The articles contained in this special issue, cover the following topics: Mathematical models of concurrency, Specification languages, Theory of programming, Parallel algorithms, Model checking and testing, Multi-agent systems, Rough sets, Object-oriented approaches, Knowledge management, Knowledge discovery and data mining, Soft computing, Information technology and management, as well as Applications.In order to provide the readers with a better insight into this special issue, we enclose below brief overviews of the accepted papers.The first two articles 'A Classifier Based on a Decision Tree with Verifying Cuts' and 'Classifiers for Behavioral Patterns Identification Induced from Huge Temporal Data', written by members of the Jan G. Bazan's group, are devoted to constructing hierarchical classifiers.The first one considers building decision trees based on additional cuts, while the second one deals with temporal data.

This special issue of Fundamenta Informaticae is dedicated to papers selected from the 24th International Workshop on CONCURRENCY, SPECIFICATION, AND PROGRAMMING (CS&P 2015), which was held in September 28 -30, 2015 in Rzeszów, Poland.After the event, some authors of the papers presented at the workshop were invited to submit a revised and extended version of their papers, which underwent another reviewing process to guarantee that the revised papers meet the standards of FUNDAMENTA INFORMATICAE.Eventually, twelve papers have been selected for publication in this special issue, which gives a representative account of current issues and topics related to Concurrency, Specification, and Programming.A complete collection of the contributions to CS&P 2015 has been edited by scientists of University of Rzeszów and published before the workshop as Proceedings.The article 'Comparison of Heuristics for Optimization of Association Rules' by Fawaz Alsolami, Talha Amin, Igor Chikalov, Mikhail Moshkov, and Beata Zielosko, includes several heuristics for construction of association rules.The presented experimental results show that the difference concerning the length or coverage obtained by the best heuristic and optimal ones (constructed using dynamic programming algorithms) are small.In the paper 'Specialized Predictor for Reaction Systems with Context Properties' Roberto Barbuti, Roberta Gori, Francesca Levi, and Paolo Milazzo consider reaction systems.They revise the notion of formula based predictor by defining a specialized version that assumes the environment to provide molecules according to what expressed by a temporal logic formula.As an application, specialized formula based predictors are used to give theoretical grounds to a model of gene regulation.

This special issue is dedicated to papers selected from the 36th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency (Petri Nets 2015), which was held June 21-26, 2015 in Brussels, Belgium.

The paper deals with the concrete planning problem – a stage of the web service composition in the PlanICS framework. We present several known and new methods of concrete planning including those based on Satisfiability Modulo Theories (SMT), Genetic Algorithm (GA), as well as methods combining SMT with GA and other nature-inspired algorithms such as Simulated Annealing (SA) and Generalised Extremal Optimization (GEO). The discussion of all the approaches is supported by the complexity analysis, extensive experimental results, and illustrated by a running example.

The article introduces a parametric extension of Action-Restricted Computation Tree Logic called pmARCTL. A symbolic fixed-point algorithm providing a solution to the exhaustive parameter synthesis problem is proposed. The parametric approach allows for an in-depth system analysis and synthesis of the correct parameter values. The time complexity of the problem and the algorithm is provided. An existential fragment of pmARCTL (pmEARCTL) is identified, in which all of the solutions can be generated from a minimal and unique base. A method for computing this base using symbolic methods is provided. The prototype tool SPATULA implementing the algorithm is applied to the analysis of three benchmarks: faulty Train-Gate-Controller, Peterson’s mutual exclusion protocol, and a generic pipeline processing network. The experimental results show efficiency and scalability of our approach compared to the naive solution to the problem.

The paper deals with symbolic approaches to bounded model checking (BMC) for the existential fragment of linear temporal logic extended with the epistemic component (ELTLK), interpreted over interleaved interpreted systems. Two translations of BMC for ELTLK to SAT and to operations on BDDs are presented. The translations have been implemented, tested, and compared with each other as well as with another tool on several benchmarks for MAS. Our experimental results reveal advantages and disadvantages of SAT- versus BDD-based BMC for ELTLK.

We show how to synthesise parameter values under which a given property, expressed in a certain extension of CTL, called RTCTLP , holds in a parametric timed Kripke structure. We prove the decidability of parameter synthesis for RTCTLP by showing how

The paper deals with the concrete planning problem (CPP) – a stage of the Web Service Composition (WSC) in the PlanICS framework. The complexity of the problem is discussed. A novel SMT-based approach to CPP is defined and its performance is compared to the standard Genetic Algorithm (GA) and the OpenOpt numerical toolset planner in the framework of the PlanICS system. The discussion of all the approaches is supported by extensive experimental results.

This is the second part of the sixteenth special issue of Fundamenta Informaticae, based on the CONCURRENCY SPECIFICATION AND PROGRAMMING (CS&P) workshop, in succession to the fifteenth special issue published in 2013.This part contains 15 selected and extended versions out of 42 papers presented at the meeting that took place in Warsaw from the 25th to the 27th of September 2013.As it was the case of all the previous special issues of Fundamenta Informaticae, based on CS&P, the papers have been selected on the basis of a review process admitted by international scientific periodicals.A complete collection of the contributions has been edited by scientists of the Warsaw University and published before the workshop as Proceedings.Therefore, this is a continuation of the tradition of the former CS&P workshops, whose participants had been supplied with proceedings in the form of technical reports during the meetings.The papers contained in both the parts of the special issue cover the following topics: mathematical models of concurrent systems, parallel algorithms, model checking, multi-agent systems, rough sets, workflow systems, mereological approaches, knowledge management, knowledge discovery and data mining, neural networks, machine learning, robotics, genetic algorithms, as well as soft computing and some applications.The CS&P workshops, being held every even year in Germany and every odd year in Poland, are supported by two universities: the Warsaw University and the Humboldt University of Berlin on the basis of an exchange programme.Initiated by computer science and mathematical logic interest groups affiliated to the two universities in the mid-seventies of the XX century, the workshops were suspended for some years in the eighties and resumed in 1992 in the extended form of participation: they evolved from bilateral meetings to the meetings hosting researchers also from a number of countries other than Germany and Poland.The scope of the subjects has been broadened too: from linguistic and logical issues initially to such research areas as the ones mentioned above.

This special issue is dedicated to selected papers from the 32nd International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, which took place in June 2011 in Newcastle upon Tyne, UK.In a careful reviewing process, 17 regular contributions have been accepted for presentation at the conference among 49 submissions.Then, after the conference, a collection of papers published in the proceedings was selected with the help of the Program Committee members, and the authors were invited to revise and extend their contributions for this special issue.Next, the extended submissions have been examined in another independent reviewing process involving two review rounds to meet the standards of FUNDAMENTA INFORMATICAE.Finally, six contributions have been accepted for publication.The accepted papers give a good overview of some recent developments in the area of Petri nets and other models of concurrency.

Automating the composition of web services is an object of a growing interest. In our paper [13] we proposed a method for converting the problem of the composition to the problem of building a graph of worlds consisting of formally defined objects, and presented the first phase of this composition aimed at building a graph of types of services (an abstract graph). In this work we propose a method of replacing abstract flows of this graph by sequences of concrete services able to satisfy the user’s request. The method is based on SAT-based reachability checking for (timed) automata with discrete data and parametric assignments.

This is the second part of the fourteenth special issue of Fundamenta Informaticae devoted to the CONCURRENCY SPECIFICATION AND PROGRAMMING (CS&P) workshop, in succession to the thirteenth special issue published in 2011. Similarly to the first issue, the second one contains selected and extended versions of 11 out of 54 papers presented at the meeting that took place in Putusk, Poland, from 28 to 30 September 2011. As it was the case of all the previous special issues of Fundamenta Informaticae based on CS&P, all the papers have been very carefully selected on the basis of a review process admitted by international scientific periodicals. A complete collection of the contributions has been published before the workshop by University of Biaystok as Proceedings. This has been a continuation of the tradition of the former CS&P workshops, whose participants had been supplied with proceedings in the form of technical reports at the meetings. The papers of this issue cover the following important topics: mathematical models of concurrent systems, Petri nets in particular, parallel algorithms, model checking, theory of formal languages, specification languages, multi-agent systems, rough sets, objectoriented approaches, knowledge management, knowledge discovery, and data mining, as well as soft computing.

This paper makes two contributions to the verification of multi-agent systems modelled by interleaved interpreted systems. Firstly, the paper presents theoretical underpinnings of the SAT-based bounded model checking (BMC) approach for LTL extended w

The paper presents a prototype toolset to planning by automatic composition of web services. The main idea consists in arranging the composition into two main phases: abstract and concrete one, as well as to handle fully declarative user queries. The

This special issue is dedicated to selected papers from the 31st International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, which took place in June 2010 in Braga (Portugal).In a careful reviewing process, 16 regular contributions have been accepted among 50 submissions for this conference.Then, after the conference, about one fourth of the papers published in the proceedings was selected with the help of the Program Committee members, and the authors were invited to revise and extend their contributions for this special issue.Next, the extended submissions have been examined in another independent reviewing process to meet the standards of FUNDAMENTA INFORMATICAE.Finally, nine contributions of which 2 are tool papers have been accepted for publication.The accepted papers give a good overview of some recent developments in the area of Petri nets and other models of concurrency.

We investigate the problem of locally monitoring contract regulated behaviours in agent-based web services. We encode contract clauses in service specifications by using extended timed automata. We propose a non intrusive local monitoring framework along with an API to monitor the fulfillment (or violation) of contractual obligations. A key feature of the framework is that it is fully symbolic thereby providing a scalable solution to monitoring. At runtime execution steps generated by the service are passed as input to the runtime monitor. Conformance of the execution against the service specification is checked using a symbolically represented extended timed automaton. This allows us to monitor service behaviours over large state spaces generated by multiple, long running contracts. We illustrate our methodology by monitoring a service composition scenario from the vehicle repair domain, and report on the experimental results.

In the paper we present a bounded model checking for 1-safe Petri nets and properties expressed in LTL and the universal fragment of CTL, based on binary decision diagrams. The presented experimental results show that we have obtained a technique whi

This is the second part of the thirteenth special issue of Fundamenta Informaticae devoted to the CONCURRENCY SPECIFICATION AND PROGRAMMING (CS&P) workshop, in succession to the twelfth special issue published in 2010. This part contains selected and extended versions of 7 out of 40 papers presented at the meeting that took place in Helenenau, Germany, from the 27th to the 29th of September 2010. As it was the case of all the previous special issues of Fundamenta Informaticae based on the CS&P workshop, the papers have been selected on the basis of a review process admitted by international scientific periodicals. A complete collection of the contributions has been published before the workshop by the Humboldt University of Berlin as Proceedings. Therefore, this a continuation of the tradition of the former CS&P workshops, whose participants had been supplied with proceedings in the form of technical reports at the meetings. The papers contained in both parts of the special issue cover the following topics: mathematical models of concurrent systems, Petri nets in particular, parallel algorithms, model checking and testing, theory of programming, specification languages, multiagent systems, rough sets, object-oriented approaches, knowledge management, knowledge discovery and data mining, as well as soft computing and some applications.

This issue is dedicated to selected papers from the 30th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency which took place in June 2009 in Paris.For that conference, 19 regular contributions were selected among 46 submissions, in a careful reviewing process.

Bounded Model Checking (BMC) is an efficient technique applicable to verification of temporal properties of (timed) distributed systems. In this paper we show for the first time how to apply BMC to parametric verification of time Petri nets with discrete-time semantics. The properties are expressed by formulas of the logic PRTECTL - a parametric extension of the existential fragment of Computation Tree Logic (CTL).

We investigate partial order reduction techniques for the verification of multi-agent systems. We investigate the case of interleaved interpreted systems. These are a particular class of interpreted systems, a mainstream MAS formalism, in which only one action at the time is performed in the system. We present a notion of stuttering-equivalence and prove the semantical equivalence of stuttering-equivalent traces with respect to linear and branching time temporal logics for knowledge without the next operator. We give algorithms to reduce the size of the models before the model checking step and show preservation properties. We evaluate the technique by discussing implementations and the experimental results obtained against well-known examples in the MAS literature.

This is the second part of the twelfth special issue of Fundamenta Informaticae devoted to the CONCURRENCY SPECIFICATION AND PROGRAMMING (CS&P) workshop, in succession to the eleventh special issue published in 2009. Similarly to the first issue, the second one contains selected and extended versions of 9 out of 63 papers presented at the meeting that took place in Krakw-Przegorzay, Poland, from 28 to 30 September 2009. As it was the case of all the previous special issues of Fundamenta Informaticae based on CS&P, all the papers have been very carefully selected on the basis of a review process admitted by international scientific periodicals. A complete collection of the contributions has been published before the workshop by University of Warsaw as Proceedings. This has been a continuation of the tradition of the former CS&P workshops, whose participants had been supplied with proceedings in the form of technical reports at the meetings. The papers of this issue cover the following important topics: mathematical models of concurrent systems, Petri nets in particular, parallel algorithms, model checking, theory of formal languages, specification languages, multi-agent systems, rough sets, object-oriented approaches, knowledge management, knowledge discovery, and data mining, as well as soft computing.

In this paper we offer a methodology allowing for simulation of security protocols, implemented in the higher-level language Estelle, using scenarios designed for external attacks. To this aim we apply a translation of specifications of security protocols from Common Syntax to Estelle and an encoding of schemes of attacks into Estelle scenarios. We show that such an intelligent simulation may efficiently serve for validating security protocols.

A new approach to verification of timed security protocols is given. The idea consists in modelling a finite number of users (including an intruder) of the computer network and their knowledge about secrets by timed automata. The runs of the product

The paper presents a new approach to model checking of systems specified in UML. All the executions of an UML system (unfolded to a given depth) are encoded directly into a boolean propositional formula, satisfiability of which is checked using a SAT-solver. Contrary to other UML verification tools we do not use any of the existing model checkers as we do not translate UML specifications into an intermediate formalism. The method has been implemented as the (prototype) tool BMC4UML and some experimental results are presented.

The ”state explosion problem” can be alleviated by using partial order reduction techniques. These methods rely on expanding only a fragment of the full state space of a program, which is sufficient for verifying the formulas of temporal logics LTL −X or CTL −X * (i.e., LTL or CTL * without the next state operator). This is guaranteed by preserving either a stuttering maximal trace equivalence or a stuttering bisimulation between the full and the reduced state space. Since a stuttering bisimulation is much more restrictive than a stuttering maximal trace equivalence, resulting in less powerful reductions for CTL −X * , we study here partial order reductions that preserve equivalences ”in-between”, in particular a stuttering simulation which is induced by the universal fragment of CTL: −X * , called ACTL −X * The reductions generated by our method preserve also branching simulation and weak simulation, but surprisingly, they do not appear to be included into the reductions obtained by Peled's method for verifying LTL −X properties. Therefore, in addition to ACTL −X * reduction method we suggest also an improvement of the LTL −X reduction method. Moreover, we prove that reduction for concurrency fair version of ACTL −X * is more efficient than for ACTL −X * .

Partial order temporal logics interpreted on trace systems have been shown not to have finitary complete axiomatizations due to the fact that the complexity of their decidability problem is in II 1 1 . This paper gives infinitary complete proof systems for several temporal logics on trace systems e.g. Computation Tree Logic with past operators and an essential subset of Interleaving Set Temporal Logic.

A temporal logic for causality (T/sub LC/) is introduced. The logic is interpreted over causal structures corresponding to partial order executions of programs. For causal structures describing the behavior of a finite fixed set of processes, a T/sub LC/-formula can, equivalently, be interpreted over their linearizations. The main result of the paper is a tableau construction that gives a singly-exponential translation from a T/sub LC/ formula /spl psi/ to a Streett automaton that accepts the set of linearizations satisfying /spl psi/. This allows both checking the validity of T/sub LC/ formulas and model-checking of program properties. As the logic T/sub LC/ does not distinguish among different linearizations of the same partial order execution, partial order reduction techniques can be applied to alleviate the state-space explosion problem of model-checking.