We descrive some theoretical and practical aspects we had to solve while developing of a toolset to prototype (symbolically execute) algebraic specifications of concurrent, systems and languages. The methodology used in writing such specifications has allowed us to develop efficient specialized algorithms and strategies which we have implemented. The resulting prototype is being used as a research tool and its use, especially in conjunction with other existing verification tools, seems very promising.

A powerful paradigm is presented for defining semantics of data types which can assign sensible semantics also to data representing processes. Processes are abstractly viewed as elements of observable sort in an algebraic structure, independently of the language used for their description. In order to define process semantics depending on the observations we introduce observational structures, essentially first-order structures where we specify how processes are observed. Processes are observationally related by means of experiments considered similar depending on a similarity law and relations over processes are propagated to relations over elements of non-observable sort by a propagation law. Thus an observational equivalence is defined, as union of all observational relations, which can be seen as a very abstract generalization of bisimulation equivalences introduced by David Park.Though being general and abstract our construction allows to extend and improve interesting classical results. For example it is shown that for finitely observable structures the observational equivalence is obtainable as a limit of a denumerable chain of iterations; our conditions, which apply to algebraic structures in general, when instantiated in the case of labelled transition systems, are more liberal than the finitely branching condition. More importantly, we show how to associate with an observational structure various modal observational logics, related to sets of experiment schemas, that we call pattern sets. The main result of the paper proves that for any family of pattern sets representing the simulation law the corresponding modal observational logic is a Hennessy-Milner logic: two observable objects are observationally equivalent if and only if they satisfy the same set of modal observational formulas. Indeed observational logics generalize to first-order structures various modal logics for labelled transition systems. Applications are shown to multilevel parallelism, higher-order concurrent calculi, distributed and branching bisimulation.The theory presented in the paper is not at all confined to give semantics of processes. Indeed it provides a general semantic paradigm for abstract data type specifications, where some data are processes. In order to support this claim, in the final section we briefly consider algebraic specifications and give small examples of specifications integrating processes, data types and functions.

Article Free Access"One sugar cube, please" or selection strategies in the Buchberger algorithm Share on Authors: Alessandro Giovini Dipartimento di Matematica - Via L. B. Alberti 4 - Genova Dipartimento di Matematica - Via L. B. Alberti 4 - GenovaView Profile , Teo Mora Dipartimento di Matematica - Via L. B. Alberti 4 - Genova Dipartimento di Matematica - Via L. B. Alberti 4 - GenovaView Profile , Gianfranco Niesi Dipartimento di Matematica - Via L. B. Alberti 4 - Genova Dipartimento di Matematica - Via L. B. Alberti 4 - GenovaView Profile , Lorenzo Robbiano Dipartimento di Matematica - Via L. B. Alberti 4 - Genova Dipartimento di Matematica - Via L. B. Alberti 4 - GenovaView Profile , Carlo Traverso Dipartimento di Matematica - Via Buonarroti 2 - Pisa Dipartimento di Matematica - Via Buonarroti 2 - PisaView Profile Authors Info & Claims ISSAC '91: Proceedings of the 1991 international symposium on Symbolic and algebraic computationJune 1991 Pages 49–54https://doi.org/10.1145/120694.120701Online:01 June 1991Publication History 67citation634DownloadsMetricsTotal Citations67Total Downloads634Last 12 Months27Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF